Module Qcert.Utils.Apply


This module provides support for operators application.

Require Import List.

Section Apply.
  Context {A:Set}.

  Definition apply_unary (f: A -> option A) (dl: list A) : option A :=
    match dl with
    | d :: nil => f d
    | _ => None
    end.
  Definition apply_binary (f: A -> A -> option A) (dl: list A) : option A :=
    match dl with
    | d1 :: d2 :: nil => f d1 d2
    | _ => None
    end.
  Definition apply_ternary (f: A -> A -> A -> option A) (dl: list A) : option A :=
    match dl with
    | d1 :: d2 :: d3 :: nil => f d1 d2 d3
    | _ => None
    end.
End Apply.