diff options
Diffstat (limited to 'test-suite/output/Notations3.out')
| -rw-r--r-- | test-suite/output/Notations3.out | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 436e97e9f..e6a6e0288 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -194,9 +194,11 @@ pair (prod nat (prod nat nat))) (prod (prod nat nat) nat) fun x : nat => if x is n .+ 1 then n else 1 : nat -> nat +{'{{x, y}} : nat * nat | x + y = 0} + : Set exists2' {{x, y}}, x = 0 & y = 0 : Prop -exists2 x : nat * nat, +myexists2 x : nat * nat, let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y : Prop fun '({{x, y}} as z) => x + y = 0 /\ z = z @@ -225,3 +227,11 @@ fun N : nat => [N | N + 0] : nat -> nat * (nat -> nat) fun S : nat => [[S | S + S]] : nat -> nat * (nat -> nat) +{I : nat | I = I} + : Set +{'I : True | I = I} + : Prop +{'{{x, y}} : nat * nat | x + y = 0} + : Set +exists2 '{{y, z}} : nat * nat, y > z & z > y + : Prop |