diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-18 15:09:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-18 15:51:02 +0200 |
| commit | fd0cd480a720cbba15de86bbc9cad74ba6d89675 (patch) | |
| tree | 157da3e6f8a88f752fe516e34d70d58a7864021c /test-suite/output/Notations3.out | |
| parent | 2042daa9a6e13cbb9636a62812015749d95c2283 (diff) | |
A new step on using alpha-conversion in printing notations.
A couple of bugs have been found.
Example #4932 is now printing correctly in the presence of multiple
binders (when no let-in, no irrefutable patterns).
Diffstat (limited to 'test-suite/output/Notations3.out')
| -rw-r--r-- | test-suite/output/Notations3.out | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 6b2177830..c10c78652 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -38,3 +38,44 @@ forall x : nat, {|x | x > 0|} : Prop exists2 x : nat, x = 1 & x = 2 : Prop +fun n : nat => +foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + z = 0) z y x) + : nat -> Prop +fun n : nat => +foo2 n (fun a b c : nat => (fun _ _ _ : nat => a + b + c = 0) c b a) + : nat -> Prop +fun n : nat => +foo2 n (fun n0 y z : nat => (fun _ _ _ : nat => n0 + y + z = 0) z y n0) + : nat -> Prop +fun n : nat => +foo2 n (fun x n0 z : nat => (fun _ _ _ : nat => x + n0 + z = 0) z n0 x) + : nat -> Prop +fun n : nat => +foo2 n (fun x y n0 : nat => (fun _ _ _ : nat => x + y + n0 = 0) n0 y x) + : nat -> Prop +fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2 + : nat -> Prop +fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2 + : nat -> Prop +fun n : nat => {|n, n0 | fun _ _ _ : nat => n + n0 = 0 |}_2 + : nat -> Prop +fun n : nat => +foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x) + : nat -> Prop +fun n : nat => +foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x) + : nat -> Prop +fun n : nat => {|n, fun _ : nat => 0 = 0 |}_3 + : nat -> Prop +fun n : nat => {|n, fun _ : nat => n = 0 |}_3 + : nat -> Prop +fun n : nat => foo3 n (fun x _ : nat => ETA z : nat, (fun _ : nat => x = 0)) + : nat -> Prop +fun n : nat => {|n, fun _ : nat => 0 = 0 |}_4 + : nat -> Prop +fun n : nat => {|n, fun _ : nat => n = 0 |}_4 + : nat -> Prop +fun n : nat => foo4 n (fun _ _ : nat => ETA z : nat, (fun _ : nat => z = 0)) + : nat -> Prop +fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0)) + : nat -> Prop |