blob: 2153ef47c0f834bf482ce350b738b5eb3a1b073e (
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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
type constr_ast =
Pair of constr_ast * constr_ast
| Prod of binder list * constr_ast
| Lambda of binder list * constr_ast
| Let of string * constr_ast * constr_ast
| LetCase of binder list * constr_ast * constr_ast
| IfCase of constr_ast * constr_ast * constr_ast
| Eval of red_fun * constr_ast
| Infix of string * constr_ast * constr_ast
| Prefix of string * constr_ast
| Postfix of string * constr_ast
| Appl of constr_ast * constr_arg list
| ApplExpl of string list * constr_ast list
| Scope of string * constr_ast
| Qualid of string list
| Prop | Set | Type
| Int of string
| Hole
| Meta of string
| Fixp of fix_kind *
(string * binder list * constr_ast * string option * constr_ast) list *
string
| Match of case_item list * constr_ast option *
(pattern list * constr_ast) list
and red_fun = Simpl
and binder = string * constr_ast
and constr_arg = string option * constr_ast
and fix_kind = Fix | CoFix
and case_item = constr_ast * (string option * constr_ast option)
and pattern =
PatAs of pattern * string
| PatType of pattern * constr_ast
| PatConstr of string * pattern list
| PatVar of string
let mk_cast c t =
if t=Hole then c else Infix(":",c,t)
let mk_lambda bl t =
if bl=[] then t else Lambda(bl,t)
|
