diff options
Diffstat (limited to 'test-suite/output/Notations2.out')
| -rw-r--r-- | test-suite/output/Notations2.out | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 121a369a94..0e5f399036 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -17,10 +17,8 @@ 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, -let b := 1 in -let c := b in -let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d +∃ (x y : nat) (b := 1) (c := b) (d := 2) (z : nat) (e := 3) (f := 4), +x + y = z + d : Prop ∀ n p : nat, n + p = 0 : Prop |