diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-14 01:27:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:04 +0100 |
| commit | a18e87f6a929ce296f8c277b310e286151e06293 (patch) | |
| tree | 703657d008ea6a21e7e230b3b27a9ce2618e0f65 /test-suite/output/Notations3.out | |
| parent | d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 (diff) | |
Allowing variables used in recursive notation to occur several times in pattern.
This allows for instance to support recursive notations of the form:
Notation "! x .. y # A #" :=
(((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..)
(at level 200, x binder).
Diffstat (limited to 'test-suite/output/Notations3.out')
| -rw-r--r-- | test-suite/output/Notations3.out | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index e114ea894..5bfdec989 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -163,3 +163,13 @@ exists_true (x : nat) (A : Type) (R : A -> A -> Prop) : Prop {{{{True, nat -> True}}, nat -> True}} : Prop * Prop * Prop +{{D 1, 2}} + : nat * nat * (nat * nat * (nat * nat)) +! a b : nat # True # + : Prop * (Prop * Prop) +!!!! a b : nat # True # + : Prop * Prop * (Prop * Prop * Prop) +@@ a b : nat # a = b # b = a # + : Prop * Prop +exists_non_null x y z t : nat , x = y /\ z = t + : Prop |