Skip to main content

🍬 Script_list.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Utils.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.

The function [empty] is valid.
The function [cons_value] is valid.