diff options
Diffstat (limited to 'test-suite/output/Notations2.out')
-rw-r--r-- | test-suite/output/Notations2.out | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 0e5f39903..6ffe56e11 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -17,8 +17,9 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y ∃ n p : nat, n + p = 0 : Prop let a := 0 in -∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat) (e := 3) (f := 4), -x + y = z + d +∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat), +let e := 3 in +let f := 4 in x + y = z + d : Prop ∀ n p : nat, n + p = 0 : Prop |