🍃 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.