diff options
| author | Pierre-Marie Pédrot | 2020-03-05 12:36:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-05 12:36:54 +0100 |
| commit | a3d1646b59b4233b87b902b627583cf9f028311d (patch) | |
| tree | aa60345941febb549aa3be6d0440e22bc4091b48 /test-suite | |
| parent | 33ab70ac3a8d08afb67d9602d7c23da7133ad0f4 (diff) | |
| parent | eb9d633b8b4e8a096f28c28877b6aa888dffe74a (diff) | |
Merge PR #11602: Adding support for an "only parsing" modifier in "where"-based notation
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot
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. |