diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-19 10:58:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-19 11:57:21 +0200 |
| commit | a67bd7f93224c61b6a59459ea1114a6670daa857 (patch) | |
| tree | 59ec2885f0059baa24403d37eaf559b59e5f82bb /test-suite/output/Notations3.out | |
| parent | b663b735adaf546192ff5b25b608dda55e05f3d8 (diff) | |
Taking into account binding patterns when agglutinating sequences of binders.
Supporting accordingly printing of sequences of binders including binding
patterns.
Diffstat (limited to 'test-suite/output/Notations3.out')
| -rw-r--r-- | test-suite/output/Notations3.out | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 950382d57..360f37967 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -96,3 +96,5 @@ 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 +tele (t : Type) '(y, z) (x : t0) := tt + : forall t : Type, nat * nat -> t -> fpack |