blob: 8dadace77d818318502b3d37089a24eacc1ec19e (
plain)
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
|
Module Type ELEM.
Parameter A : Set.
Parameter x : A.
End ELEM.
Module Nat.
Definition A := nat.
Definition x := 0.
End Nat.
Module List (X: ELEM).
Inductive list : Set :=
| nil : list
| cons : X.A -> list -> list.
Definition head (l : list) := match l with
| nil => X.x
| cons x _ => x
end.
Definition singl (x : X.A) := cons x nil.
Lemma head_singl : forall x : X.A, head (singl x) = x.
auto.
Qed.
End List.
Module N := List Nat.
|
