Skip to content
Snippets Groups Projects
Select Git revision
  • 3c754621e8348d656ccc11e1a50f636caae114fb
  • master default protected
2 results

modureserl

Paul Wild's avatar
Paul Wild authored
Change Inductive stepn to mstep in Language.v, move stepn back to
CompatibilityUnary.v.
Define new evaluation closure (using mstep), prove new Lemma eval_simpl.
3c754621
History
Name Last commit Last update