blob: 28ea99dfefc7da0f2658812b2533823a6c74671d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* Classes and sections *)
Section OPT.
Variable A: Type.
Inductive MyOption: Type :=
| MyNone: MyOption
| MySome: A -> MyOption.
Class Opt: Type := {
f_opt: A -> MyOption
}.
End OPT.
Definition f_nat (n: nat): MyOption nat := MySome _ n.
Instance Nat_Opt: Opt nat := {
f_opt := f_nat
}.
|
