diff options
| author | Hugo Herbelin | 2020-02-14 13:01:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-04 11:56:40 +0100 |
| commit | fb9442de3a7f5cab102f33a342a5fc7f63cd8f1c (patch) | |
| tree | 5d4aa2080df69642bd2121e8c4a2576a2b9cfbb5 /test-suite | |
| parent | 89f111f2e15d8cab61495a419f0c9f7ae95e086a (diff) | |
Adding support for an "only parsing" modifier in "where"-based notations.
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Inductive.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Inductive.v | 8 |
2 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 8ff571ae55..ff2556c5dc 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -5,3 +5,5 @@ Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x Arguments foo _%type_scope Arguments Foo _%type_scope +myprod unit bool + : Set diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index 9eec9a7dad..db1276cb6c 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -5,3 +5,11 @@ Fail Inductive list' (A:Set) : Set := (* Check printing of let-ins *) #[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo. Print foo. + +(* Check where clause *) +Reserved Notation "x ** y" (at level 40, left associativity). +Inductive myprod A B := + mypair : A -> B -> A ** B + where "A ** B" := (myprod A B) (only parsing). + +Check unit ** bool. |