blob: db1276cb6c08276523799d396eb4578629ea434d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Fail Inductive list' (A:Set) : Set :=
| nil' : list' A
| cons' : A -> list' A -> list' (A*A).
(* 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.
|
