forked from formal-land/coq-of-ocaml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
sum_types.v
53 lines (40 loc) · 1.08 KB
/
sum_types.v
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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
(** File generated by coq-of-ocaml *)
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Inductive t1 : Set :=
| C1 : int -> t1
| C2 : bool -> int -> t1
| C3 : t1.
Definition n_value : t1 := C2 false 3.
Definition m_value : bool :=
match n_value with
| C2 b_value _ => b_value
| _ => true
end.
Inductive t2 (a : Set) : Set :=
| D1 : t2 a
| D2 : a -> t2 a -> t2 a.
Arguments D1 {_}.
Arguments D2 {_}.
Fixpoint of_list {A : Set} (l_value : list A) : t2 A :=
match l_value with
| [] => D1
| cons x_value xs => D2 x_value (of_list xs)
end.
Fixpoint sum (l_value : t2 int) : int :=
match l_value with
| D1 => 0
| D2 x_value xs => Z.add x_value (sum xs)
end.
Definition s_value {A : Set} (function_parameter : A) : int :=
let '_ := function_parameter in
sum (of_list [ 5; 7; 3 ]).
Parameter t3 : Set.
Parameter t4 : forall (a : Set), Set.
Inductive t5 : Set :=
| C : t5.
Inductive single_string : Set :=
| Single : string -> single_string.
Definition get_string (s_value : single_string) : string :=
let 'Single s_value := s_value in
s_value.