Module `Lemmas`

Proofs attached to a constant

type t: Lemmas.t represents a constant that is being proved, usually interactively

val set_endline_tactic : Genarg.glob_generic_argument -> t -> t: set_endline_tactic tac lemma set ending tactic for lemma

val pf_map : (Declare.Proof.t -> Declare.Proof.t) -> t -> t: pf_map f l map the underlying proof object

val pf_fold : (Declare.Proof.t -> 'a) -> t -> 'a: pf_fold f l fold over the underlying proof object

val by : unit Proofview.tactic -> t -> t * bool: by tac l apply a tactic to l

module Proof_ending : sig ... end: Creating high-level proofs with an associated constant

module Info : sig ... end

val start_lemma : name:Names.Id.t -> poly:bool -> ?⁠udecl:UState.universe_decl -> ?⁠info:Info.t -> ?⁠impargs:Impargs.manual_implicits -> Evd.evar_map -> EConstr.types -> t: Starts the proof of a constant

val start_dependent_lemma : name:Names.Id.t -> poly:bool -> ?⁠udecl:UState.universe_decl -> ?⁠info:Info.t -> Proofview.telescope -> t

type lemma_possible_guards = int list list

val start_lemma_with_initialization : ?⁠hook:Declare.Hook.t -> poly:bool -> scope:Declare.locality -> kind:Decls.logical_kind -> udecl:UState.universe_decl -> Evd.evar_map -> (bool * lemma_possible_guards * Constr.t option list option) option -> Declare.Recthm.t list -> int list option -> t: Pretty much internal, used by the Lemma / Fixpoint vernaculars

Saving proofs

val save_lemma_admitted : lemma:t -> unit
val save_lemma_proved : lemma:t -> opaque:Declare.opacity_flag -> idopt:Names.lident option -> unit

module Internal : sig ... end: To be removed, don't use!

val save_lemma_admitted_delayed : proof:Declare.proof_object -> info:Info.t -> unit: Special cases for delayed proofs, in this case we must provide the proof information so the proof won't be forced.

val save_lemma_proved_delayed : proof:Declare.proof_object -> info:Info.t -> idopt:Names.lident option -> unit