diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-10 17:10:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:03 +0100 |
| commit | 9324dcf528f16be420b08c376a6580c8987f50fd (patch) | |
| tree | 21eda2f66226c0f9da6a9e6efd623048c4bb983d /test-suite/output | |
| parent | 6b9a9124d3bd24fe9305df613547139f6f609c60 (diff) | |
Using name given by user to name a 'pat, if any.
This works for contexts in Definition and co, but not yet for "fun" and co.
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/PatternsInBinders.out | 6 | ||||
| -rw-r--r-- | test-suite/output/PatternsInBinders.v | 5 |
2 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 6b09c3308..8a6d94c73 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -39,3 +39,9 @@ forall '(x, y) '(z, t), swap (x, y) = (z, t) : Prop fun (pat : nat) '(x, y) => x + y = pat : nat -> nat * nat -> Prop +f = fun x : nat => x + x + : nat -> nat + +Argument scope is [nat_scope] +fun x : nat => x + x + : nat -> nat diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 0bad472f4..d671053c0 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -67,3 +67,8 @@ End Suboptimal. (** Test risk of collision for internal name *) Check fun pat => fun '(x,y) => x+y = pat. + +(** Test name in degenerate case *) +Definition f 'x := x+x. +Print f. +Check fun 'x => x+x. |