blob: ee5b052811afc1ebbf94a9750fd715c80ce5f63f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Goal exists I, I = Logic.I.
Show.
Abort.
Notation f x y p q r := ((forall x, p /\ r) /\ forall y, q /\ r).
Goal f True False True False (Logic.True /\ Logic.False).
Show.
Abort.
Notation "[ x | y ; z ; .. ; t ]" := (pair .. (pair (forall x, y) (forall x, z)) .. (forall x, t)).
Goal [ I | I = Logic.I ; I = Logic.I ] = [ I | I = Logic.I ; I = Logic.I ].
Show.
Abort.
Notation "[ x & p | y ; .. ; z ; t ]" := (forall x, p -> y -> .. (forall x, p -> z -> forall x, p -> t) ..).
Goal [ I & I = Logic.I | I = Logic.I ; Logic.I = I ].
Show.
Abort.
|
