Skip to main content

Browse the archive

Revision a7ba07fa195296c228d92cb5049a3a8601d10b58 authored by Raphaël Cauderlier on 29 May 2019, 09:23:37 UTC, committed by Arvid Jakobsson on 29 November 2019, 13:40:31 UTC 
[Michocott] Formalize the typing rules of Michelson in OTT
 
TOFIX:

  Currently the syntax of Michelson is not shared with michelson.ott.
  Moreover I used `:` for the typing relation and `::` for stack
  consing whereas the documentation (and michelson.ott) use `:` for
  consing and `::` for typing.
1 parent cdc97c1
Raw File
.gitignore 
# General
.depend
.bkp/

# Coq
*.aux
*.glob
*.vo
*.lia.cache
# Generated by configure and coq_makefile
_CoqProject
Makefile
.coqdeps.d

# OCaml
*.cmi
*.cmo

# LaTeX
*.tex
*.vrb
*.toc
*.toc
*.snm
*.out
*.nav
*.aux
*.log
*.sty
# we keep *.pdf to ease sharing of slides
notes.*
*~
Makefile.conf
CoqMakefile.conf
back to top