Skip to main content

🍬 Script_list.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Definition empty {a : Set} : Script_typed_ir.boxed_list a :=
  {| Script_typed_ir.boxed_list.elements := nil;
    Script_typed_ir.boxed_list.length := 0; |}.

Definition cons_value {a : Set}
  (elt_value : a) (l_value : Script_typed_ir.boxed_list a)
  : Script_typed_ir.boxed_list a :=
  {|
    Script_typed_ir.boxed_list.elements :=
      cons elt_value l_value.(Script_typed_ir.boxed_list.elements);
    Script_typed_ir.boxed_list.length :=
      1 +i l_value.(Script_typed_ir.boxed_list.length); |}.