blob: 4f8e9018de6147a1a3df556232f3e8629ce21c72 (
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
|
(************************************************************************)
(* * 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 Constr
open Vernacexpr
(** {6 Fixpoints and cofixpoints} *)
(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
val do_fixpoint_interactive :
scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t
val do_fixpoint :
scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit
val do_cofixpoint_interactive :
scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t
val do_cofixpoint :
scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit
(************************************************************************)
(** Internal API *)
(************************************************************************)
(** Typing global fixpoints and cofixpoint_expr *)
val adjust_rec_order
: structonly:bool
-> Constrexpr.local_binder_expr list
-> Constrexpr.recursion_order_expr option
-> lident option
(** Exported for Program *)
val interp_recursive :
(* Misc arguments *)
program_mode:bool -> cofix:bool ->
(* Notations of the fixpoint / should that be folded in the previous argument? *)
lident option fix_expr_gen list ->
(* env / signature / univs / evar_map *)
(Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
(* names / defs / types *)
(Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) *
(* ctx per mutual def / implicits / struct annotations *)
(EConstr.rel_context * Impargs.manual_implicits * int option) list
(** Exported for Funind *)
type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list
val interp_fixpoint
: cofix:bool
-> lident option fix_expr_gen list
-> recursive_preentry * UState.universe_decl * UState.t *
(EConstr.rel_context * Impargs.manual_implicits * int option) list
(** Very private function, do not use *)
val compute_possible_guardness_evidences :
('a, 'b) Context.Rel.pt * 'c * int option -> int list
|
