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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
open Vernacexpr
open Constrexpr
(** {6 Inductive and coinductive types} *)
(** Entry points for the vernacular commands Inductive and CoInductive *)
type uniform_inductive_flag =
| UniformParameters
| NonUniformParameters
val do_mutual_inductive
: template:bool option
-> cumul_univ_decl_expr option
-> (one_inductive_expr * decl_notation list) list
-> cumulative:bool
-> poly:bool
-> private_ind:bool
-> uniform:uniform_inductive_flag
-> Declarations.recursivity_kind
-> unit
(** User-interface API *)
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
followed by enough pattern variables.
[Not_found] is raised if the given string isn't the qualid of
a known inductive type. *)
val make_cases : Names.inductive -> string list list
val interp_mutual_inductive_constr
: sigma:Evd.evar_map
-> template:bool option
-> udecl:UState.universe_decl
-> variances:Entries.variance_entry
-> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list
-> indnames:Names.Id.t list
-> arities:EConstr.t list
-> arityconcl:(bool * EConstr.ESorts.t) option list
-> constructors:(Names.Id.t list * Constr.constr list) list
-> env_ar_params:Environ.env
(** Environment with the inductives and parameters in the rel_context *)
-> cumulative:bool
-> poly:bool
-> private_ind:bool
-> finite:Declarations.recursivity_kind
-> Entries.mutual_inductive_entry * UnivNames.universe_binders
(************************************************************************)
(** Internal API, exported for Record *)
(************************************************************************)
val should_auto_template : Id.t -> bool -> bool
(** [should_auto_template x b] is [true] when [b] is [true] and we
automatically use template polymorphism. [x] is the name of the
inductive under consideration. *)
val template_polymorphism_candidate
: ctor_levels:Univ.LSet.t
-> Entries.universes_entry
-> Constr.rel_context
-> Sorts.t option
-> bool
(** [template_polymorphism_candidate ~ctor_levels uctx params
conclsort] is [true] iff an inductive with params [params],
conclusion [conclsort] and universe levels appearing in the
constructor arguments [ctor_levels] would be definable as template
polymorphic. It should have at least one universe in its
monomorphic universe context that can be made parametric in its
conclusion sort, if one is given. *)
val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int -> binders:int
-> EConstr.t -> Evd.evar_map
(** [nparams] is the number of parameters which aren't treated as
uniform, ie the length of params (including letins) where the env
is [uniform params, inductives, params, binders]. *)
val variance_of_entry
: cumulative:bool
-> variances:Entries.variance_entry
-> Entries.universes_entry
-> Entries.variance_entry option
(** Will return None if non-cumulative, and resize if there are more
universes than originally specified.
If monomorphic, [cumulative] is treated as [false].
*)
|
