diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-14 19:55:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:06 +0100 |
| commit | 15abe33f55b317410223bd48576fa35c81943ff9 (patch) | |
| tree | 2f0b0d3c5670fd84cea76aa58e979f5991703c59 /test-suite/output | |
| parent | bc73f267ad2da0f1e24e66cb481725be018a8ce6 (diff) | |
Refining the strategy for glueing let-ins to a sequence of binders.
To deal with existing notations starting with a "let" (see notation
"for" in output/Notation2.v) we adopt the pragmatic approach of
glueing only inner let by default.
Ideally, it might be nicer to detect if there is an overlap of
notation, and not to glue only in case of overlap. We could also
decide that a notation starting with a "let" should always be
protected by some constant, say "id", so as to avoid possible
collisions, but this would require changes user side.
Diffstat (limited to 'test-suite/output')
| -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 |