blob: 1367e5813eb14f782c94d84bb92d6446941029f4 (
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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
open Names
type existential_key = int
type metavariable = int
type case_style =
LetStyle
| IfStyle
| LetPatternStyle
| MatchStyle
| RegularStyle
type case_printing = { ind_nargs : int; style : case_style; }
type case_info = {
ci_ind : inductive;
ci_npar : int;
ci_cstr_nargs : int array;
ci_pp_info : case_printing;
}
type contents = Pos | Null
type sorts = Prop of contents | Type of Univ.universe
type sorts_family = InProp | InSet | InType
val family_of_sort : sorts -> sorts_family
type 'a pexistential = existential_key * 'a array
type 'a prec_declaration = name array * 'a array * 'a array
type 'a pfixpoint = (int array * int) * 'a prec_declaration
type 'a pcofixpoint = int * 'a prec_declaration
type cast_kind = VMcast | DEFAULTcast
type constr =
Rel of int
| Var of identifier
| Meta of metavariable
| Evar of constr pexistential
| Sort of sorts
| Cast of constr * cast_kind * constr
| Prod of name * constr * constr
| Lambda of name * constr * constr
| LetIn of name * constr * constr * constr
| App of constr * constr array
| Const of constant
| Ind of inductive
| Construct of constructor
| Case of case_info * constr * constr * constr array
| Fix of constr pfixpoint
| CoFix of constr pcofixpoint
type existential = constr pexistential
type rec_declaration = constr prec_declaration
type fixpoint = constr pfixpoint
type cofixpoint = constr pcofixpoint
val strip_outer_cast : constr -> constr
val collapse_appl : constr -> constr
val decompose_app : constr -> constr * constr list
val applist : constr * constr list -> constr
val iter_constr_with_binders :
('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
exception LocalOccur
val closedn : int -> constr -> bool
val closed0 : constr -> bool
val noccurn : int -> constr -> bool
val noccur_between : int -> int -> constr -> bool
val noccur_with_meta : int -> int -> constr -> bool
val map_constr_with_binders :
('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
val exliftn : Esubst.lift -> constr -> constr
val liftn : int -> int -> constr -> constr
val lift : int -> constr -> constr
type info = Closed | Open | Unknown
type 'a substituend = { mutable sinfo : info; sit : 'a; }
val lift_substituend : int -> constr substituend -> constr
val make_substituend : 'a -> 'a substituend
val substn_many : constr substituend array -> int -> constr -> constr
val substnl : constr list -> int -> constr -> constr
val substl : constr list -> constr -> constr
val subst1 : constr -> constr -> constr
type named_declaration = identifier * constr option * constr
type rel_declaration = name * constr option * constr
val map_named_declaration :
(constr -> constr) -> named_declaration -> named_declaration
val map_rel_declaration :
(constr -> constr) -> rel_declaration -> rel_declaration
val fold_named_declaration :
(constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a
val fold_rel_declaration :
(constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
type named_context = named_declaration list
val empty_named_context : named_context
val fold_named_context :
(named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
type section_context = named_context
type rel_context = rel_declaration list
val empty_rel_context : rel_context
val rel_context_length : rel_context -> int
val rel_context_nhyps : rel_context -> int
val fold_rel_context :
(rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
val map_context : (constr -> constr) -> named_context -> named_context
val map_rel_context : (constr -> constr) -> rel_context -> rel_context
val extended_rel_list : int -> rel_context -> constr list
val compose_lam : (name * constr) list -> constr -> constr
val decompose_lam : constr -> (name * constr) list * constr
val decompose_lam_n_assum : int -> constr -> rel_context * constr
val mkProd_or_LetIn : name * constr option * constr -> constr -> constr
val it_mkProd_or_LetIn : constr -> rel_context -> constr
val decompose_prod_assum : constr -> rel_context * constr
val decompose_prod_n_assum : int -> constr -> rel_context * constr
type arity = rel_context * sorts
val mkArity : arity -> constr
val destArity : constr -> arity
val isArity : constr -> bool
val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
val eq_constr : constr -> constr -> bool
(* Validation *)
val val_sortfam : Obj.t -> unit
val val_sort : Obj.t -> unit
val val_constr : Obj.t -> unit
val val_rctxt : Obj.t -> unit
val val_nctxt : Obj.t -> unit
|
