Skip to content

Beginning of dep translation of the translator

Guillaume Claret requested to merge guillaume-claret@michelson-dep-translation-more into master

In this branch there are:

  • Some changes on the interpreter, to type the term ks;
  • Some dependent definitions for the translator;
  • Some equality proofs on these dependent definitions;
  • New axioms to reason about existential matches in the environment file.

These axioms are not yet sufficient for all our code examples as I will also need to modify coq-of-ocaml to remove unused existential variables.

Edited by Guillaume Claret

Merge request reports