https://gitlab.com/nomadic-labs/mi-cho-coq
Raw File
Tip revision: 507e2754b90021ab00e9748f876c581a998bb827 authored by hu zhenlei on 16 March 2020, 17:00:38 UTC
Merge branch 'contract_spend' into 'master'
Tip revision: 507e275
micheline_syntax.v
Require Import String ZArith.
Require Import location.

Inductive micheline : Set :=
| SEQ (_ : list loc_micheline)
| PRIM (_ : location * location * string)
       (_ : list loc_micheline)
| STR (_ : string)
| BYTES (_ : string)
| NUMBER (_ : Z)
with
loc_micheline : Set :=
| Mk_loc_micheline : location * location * micheline -> loc_micheline.

back to top