1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
|
Require Import Coq.Strings.String.
Require Import iris.bi.bi.
Require Import iris.bi.ascii.
Local Open Scope string_scope.
(* this file demonstrates that the [|-] notation does not
conflict with the ltac notation.
*)
Section with_bi.
Context {PROP : bi}.
Variables P Q R : PROP.
Local Open Scope stdpp_scope.
Ltac pg :=
match goal with
| |- ?X => idtac X
end.
Ltac foo g :=
lazymatch g with
| |- ?T => idtac T
| ?U |- ?T => idtac U T
end.
Ltac bar :=
match goal with
| |- ?G => foo G
end.
Check "test1".
Lemma test1 : |-@{PROP} True.
Proof. bar. pg. Abort.
Check "test2".
Lemma test2 : False |-@{PROP} True.
Proof. bar. pg. Abort.
End with_bi.
|