Skip to content

Draft: Natasha comparable ty vs ty

Natasha Klaus requested to merge natasha-comparable-ty-vs-ty into master

TASK : Michelson: translate: comparable_ty vs ty

created 2 lemmas, need to prove them. Please check if lemmas correct.

in first lemma, not able to do induction on type ty, cos it is mutually defined and coq is not able to generate induction principle for it automatically.

we must ask for mutual principles as we need them, using the Scheme command, maybe this solution is not correct? I can not move forward with it, can not apply newly-defined induction principle.

Merge request reports