Skip to main content

Browse the archive

https://gitlab.com/nomadic-labs/mi-cho-coq
08 June 2021, 12:39:06 UTC
Revision d116674d67eca4b4b15d7c08efd878a8c8aa864b authored by kristinas on 11 May 2021, 09:41:59 UTC, committed by kristinas on 11 May 2021, 09:41:59 UTC 
Added README
1 parent f70493e
Raw File
Tip revision: d116674d67eca4b4b15d7c08efd878a8c8aa864b authored by kristinas on 11 May 2021, 09:41:59 UTC
Added README
Tip revision: d116674
micheline_syntax.v 
Require Import String ZArith.
Require Import location.

Inductive annotation := Mk_annot : location * location * string -> annotation.

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