pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising before class

Browse source
This commit is contained in:
Adam Chlipala 2020-04-26 14:30:18 -04:00
parent 42d5af6d2d
commit 300f78191e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
ProgramDerivation.v
View file

@ -497,7 +497,7 @@ Proof.
simplify; subst; eauto. simplify; subst; eauto.
Qed. Qed.
Hint Resolve ReplaceMethod_ok. Hint Resolve ReplaceMethod_ok : core.
(* It is OK to replace a method body if the new refines the old as a [comp]. *) (* It is OK to replace a method body if the new refines the old as a [comp]. *)
Theorem refine_method : forall state name (oldbody newbody : state -> nat -> comp (state * nat)) Theorem refine_method : forall state name (oldbody newbody : state -> nat -> comp (state * nat))