1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
Fail Inductive list' (A:Set) : Set :=
| nil' : list' A
| cons' : A -> list' A -> list' (A*A).
(* Check printing of let-ins *)
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.
(* "option is template" *)
About option.
Set Printing Universes.
About option.
(* "option is template on xxx" *)
Module DiffParams.
Fail Inductive B: Type :=
| F: A -> B with
Inductive A: Type := mkA.
Fail Inductive B := { x : nat } with
Inductive A := { y : nat }.
End DiffParams.
|
