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/output/Inductive.v | |
| 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/output/Inductive.v')
| -rw-r--r-- | test-suite/output/Inductive.v | 8 |
1 files changed, 8 insertions, 0 deletions
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. |