diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-17 09:28:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-17 14:27:18 +0200 |
| commit | b976aa1e49579b7b50cfb140cbac8cb6f4c881a7 (patch) | |
| tree | 668c698299acdde06b9c809ff427b47d507c4d06 /test-suite/output/Notations3.out | |
| parent | 152aca663d76f0cfda21ddef880050f21bfe4995 (diff) | |
More examples of recursive notations, with emphasis in reference manual.
Further work would include:
- Identify binders up to alpha-conversion (see #4932 with a list of
binders of length at least 2, or #4592 on printing notations such as
ex2).
A cool example that one could also consider supporting:
- Notation "[[ a , .. , b | .. | a , .. , b ]]" :=
(cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..).
Diffstat (limited to 'test-suite/output/Notations3.out')
| -rw-r--r-- | test-suite/output/Notations3.out | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 8b3fa3161..64317a9f8 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -25,3 +25,10 @@ ETA x y : nat, Nat.add : nat -> nat -> nat fun x y : nat => Nat.add x y : forall (_ : nat) (_ : nat), nat +ETA x y : nat, le_S + : forall x y : nat, x <= y -> x <= S y +fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f + : (forall x : nat * (bool * unit), ?T) -> + forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))} +where +?T : [x : nat * (bool * unit) |- Type] |