blob: 3e1e9ceaf12360bf75a146df89d1b52608e32f0a (
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
|
(************************************************************************)
(* * 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"]
(************************************************************************)
(** 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 -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool
(** [template_polymorphism_candidate env uctx params conclsort] is
[true] iff an inductive with params [params] and conclusion
[conclsort] 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. *)
val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t
(** [sign_level env sigma ctx] computes the universe level of the context [ctx]
as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *)
|
