pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Tweaked Ltac singletoner to display state space exploration in real time

Browse source
This commit is contained in:
Peng Wang 2016-02-22 17:53:31 -05:00
parent cc19c1708b
commit f05378e111
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 :=
repeat match goal with
| _ => apply singleton_in
(* | _ => apply singleton_in *)
| [ |- _ ?S ] => idtac S; apply singleton_in
| [ |- (_ \cup _) _ ] => apply singleton_in_other
end.

4
ModelChecking.v
View file

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