File: declarations.mli

package info (click to toggle)
coq 8.9.0-1
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, buster, sid
  • size: 30,604 kB
  • sloc: ml: 192,230; sh: 2,585; python: 2,206; ansic: 1,878; makefile: 818; lisp: 202; xml: 24; sed: 2
file content (52 lines) | stat: -rw-r--r-- 1,801 bytes parent folder | download
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
open Names
open Cic

val force_constr : constr_substituted -> constr
val force_lazy_constr_univs : Cic.constant_def -> Univ.ContextSet.t
val from_val : constr -> constr_substituted

val indirect_opaque_access : (DirPath.t -> int -> constr) ref
val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.ContextSet.t) ref

(** Constant_body *)

val body_of_constant : constant_body -> constr option
val constant_has_body : constant_body -> bool
val is_opaque : constant_body -> bool
val opaque_univ_context : constant_body -> Univ.ContextSet.t
val constant_is_polymorphic : constant_body -> bool

(* Mutual inductives *)

val mk_norec : wf_paths
val mk_paths : recarg -> wf_paths list array -> wf_paths
val dest_recarg : wf_paths -> recarg
val dest_subterms : wf_paths -> wf_paths list array
val eq_recarg : recarg -> recarg -> bool
val eq_wf_paths : wf_paths -> wf_paths -> bool

val inductive_make_projections : Names.inductive -> mutual_inductive_body ->
  Names.Projection.Repr.t array option

(* Modules *)

val empty_delta_resolver : delta_resolver

(* Substitutions *)

type 'a subst_fun = substitution -> 'a -> 'a

val empty_subst : substitution
val add_mbid : MBId.t -> ModPath.t -> substitution -> substitution
val add_mp   : ModPath.t -> ModPath.t -> substitution -> substitution
val map_mbid : MBId.t -> ModPath.t -> substitution
val map_mp   : ModPath.t -> ModPath.t -> substitution
val mp_in_delta : ModPath.t -> delta_resolver -> bool
val mind_of_delta : delta_resolver -> MutInd.t -> MutInd.t

val subst_const_body : constant_body subst_fun
val subst_mind : mutual_inductive_body subst_fun
val subst_signature :  substitution -> module_signature -> module_signature
val subst_module : substitution -> module_body -> module_body

val join : substitution -> substitution -> substitution