blob: ef05b213d86565da8a4c19e7b52577c60acd6e20 (
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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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
-> universe_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 declare_mutual_inductive_with_eliminations
: ?primitive_expected:bool
-> Entries.mutual_inductive_entry
-> UnivNames.universe_binders
-> DeclareInd.one_inductive_impls list
-> Names.MutInd.t
[@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"]
val interp_mutual_inductive_constr :
env0:Environ.env ->
sigma:Evd.evar_map ->
template:bool option ->
udecl:UState.universe_decl ->
env_ar:Environ.env ->
env_params:Environ.env ->
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 * 'a list list) list ->
env_ar_params:Environ.env ->
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
: Environ.env
-> ctor_levels:Univ.LSet.t
-> Entries.universes_entry
-> Constr.rel_context
-> Sorts.t option
-> bool
(** [template_polymorphism_candidate env ~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. If the [Template Check] flag is
false we just check that the conclusion sort is not small. *)
|
