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 : (Proof_global.t -> Proof_global.t) -> t -> t: pf_map f l map the underlying proof object

val pf_fold : (Proof_global.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 Recthm : sig ... end

module Info : sig ... end

val start_lemma : name:Names.Id.t -> poly:bool -> ?⁠udecl:UState.universe_decl -> ?⁠info:Info.t -> 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:DeclareDef.Hook.t -> poly:bool -> scope:DeclareDef.locality -> kind:Decls.logical_kind -> udecl:UState.universe_decl -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> Recthm.t list -> int list option -> t: Pretty much internal, only used in ComFixpoint

val default_thm_id : Names.Id.t

Saving proofs

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

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

val save_lemma_admitted_delayed : proof:Proof_global.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:Proof_global.proof_object -> info:Info.t -> idopt:Names.lident option -> unit