package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
val pf_map : (Declare.Proof.t -> Declare.Proof.t) -> t -> t
val pf_fold : (Declare.Proof.t -> 'a) -> t -> 'a
val by : unit Proofview.tactic -> t -> t * bool
module Proof_ending : sig ... end
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
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
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
val save_lemma_admitted_delayed : proof:Declare.proof_object -> info:Info.t -> unit
val save_lemma_proved_delayed : proof:Declare.proof_object -> info:Info.t -> idopt:Names.lident option -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct