Skip to main content

🍃 Seq.v

Environment

Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.Error_monad.
Require Proto_alpha.Environment.Pervasives.
Import Error_monad.Notations.

Reserved Notation "'t".

Inductive node (a : Set) : Set :=
| Nil : node a
| Cons : a 't a node a

where "'t" := (fun (t_a : Set) ⇒ unit node t_a).

Definition t := 't.

Arguments Nil {_}.
Arguments Cons {_}.

Parameter empty : {a : Set}, t a.

Parameter _return : {a : Set}, a t a.

Parameter cons_value : {a : Set}, a t a t a.

Parameter append : {a : Set}, t a t a t a.

Parameter map : {a b : Set}, (a b) t a t b.

Parameter filter : {a : Set}, (a bool) t a t a.

Parameter filter_map : {a b : Set}, (a option b) t a t b.

Parameter flat_map : {a b : Set}, (a t b) t a t b.

Parameter fold_left : {a b : Set}, (a b a) a t b a.

Parameter iter : {a : Set}, (a unit) t a unit.

Parameter unfold : {a b : Set}, (b option (a × b)) b t a.

Parameter first : {a : Set}, t a option a.

Parameter fold_left_e : {a b trace : Set},
  (a b Pervasives.result a trace) a t b
  Pervasives.result a trace.

Parameter fold_left_s : {a b : Set},
  (a b a) a t b a.

Parameter fold_left_es : {a b trace : Set},
  (a b Pervasives.result a trace) a t b
  Pervasives.result a trace.

Parameter iter_e : {a trace : Set},
  (a Pervasives.result unit trace) t a Pervasives.result unit trace.

Parameter iter_s : {a : Set}, (a unit) t a unit.

Parameter iter_es : {a trace : Set},
  (a Pervasives.result unit trace) t a
  Pervasives.result unit trace.

Parameter iter_ep : {a : Set},
  (a M? unit) t a M? unit.

Parameter iter_p : {a : Set}, (a unit) t a unit.