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

Merge pull request #10 from wangpengmit/pull-request-singletoner

Browse source 
Tweaked Ltac singletoner to display state space exploration in real time
This commit is contained in:
Adam Chlipala 2016-02-23 14:52:43 -05:00
commit cff5e1da35
2 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
Frap.v
View file

@ -104,7 +104,8 @@ Ltac model_check_done :=
Ltac singletoner := Ltac singletoner :=
repeat match goal with repeat match goal with
| _ => apply singleton_in (* | _ => apply singleton_in *)
| [ |- _ ?S ] => idtac S; apply singleton_in
| [ |- (_ \cup _) _ ] => apply singleton_in_other | [ |- (_ \cup _) _ ] => apply singleton_in_other
end. end.

4
ModelChecking.v
View file

@ -302,7 +302,8 @@ Qed.
Ltac singletoner := Ltac singletoner :=
repeat match goal with repeat match goal with
| _ => apply singleton_in (* | _ => apply singleton_in *)
| [ |- _ ?S ] => idtac S; apply singleton_in
| [ |- (_ \cup _) _ ] => apply singleton_in_other | [ |- (_ \cup _) _ ] => apply singleton_in_other
end. end.
@ -1572,3 +1573,4 @@ Theorem twoadd6_ok :
Proof. Proof.
twoadd. twoadd.
Qed. Qed.