Module Harpoon.Theorem

module Conf : sig ... end
module Action : sig ... end
type t
type theorem = t
type subgoal_hook = Synint.Comp.proof_state -> unit
val printf : t -> ('a, Support.Format.formatter, unit) Stdlib.format -> 'a

TODO hide this from outside of this module

Gets the cid and Store entry for this theorem.

val get_history_names : t -> string list * string list

get_history_names t = (as1, as2) where as1 are the past history items and as2 are the future history items.

Gets the cid for this theorem.

val get_entry : t -> Beluga.Store.Cid.Comp.Entry.t

Gets the Store entry for this theorem.

val get_name : t -> Beluga_syntax.Syncom.Name.t
val has_name_of : t -> Beluga_syntax.Syncom.Name.t -> bool

Checks if the theorem's name is equal to the given name.

val has_cid_of : t -> Beluga_syntax.Syncom.Id.cid_prog -> bool

Checks if the theorem's cid is equal to the given cid.

val get_statement : t -> Synint.Comp.tclo

Gets the type of the initial subgoal of this theorem. Note that this is the statement of the theorem _including_ inductive stars. To get the statement without stars, retrieve the type of the theorem in the store via its cid.

val serialize : Support.Format.formatter -> t -> unit
val next_subgoal : t -> Synint.Comp.proof_state option
val select_subgoal_satisfying : t -> (Synint.Comp.proof_state -> bool) -> Synint.Comp.proof_state option
val dump_proof : Support.Format.formatter -> t -> unit
val show_proof : t -> unit
val show_subgoals : t -> unit
val defer_subgoal : t -> unit
val subgoals : t -> Synint.Comp.proof_state list
val count_subgoals : t -> int
val apply : t -> Action.t -> unit

Executes the given action on this theorem, and records the action to the theorem's history.

val history_step_forward : t -> bool

history_step_forward theorem_state steps forward in the theorem state's action history, redoing the latest undone action. Returns false if no action was redone.

val history_step_backward : t -> bool

history_step_backward theorem_state steps backward in the theorem state's action history, undoing the latest done action. Returns false if no action was undone.

val apply_subgoal_replacement : t -> string -> Synint.Comp.proof_state -> (Synint.Comp.proof -> Synint.Comp.proof) -> Synint.Comp.proof_state -> unit

Replaces the subgoal with another, solving it by transforming an incomplete proof for the new subgoal. Interally this uses `apply` and so records theorem history, using the given action name.

val rename_variable : Beluga_syntax.Syncom.Name.t -> Beluga_syntax.Syncom.Name.t -> [ `comp | `meta ] -> t -> Synint.Comp.proof_state -> bool

Renames the given variable at the given level. Returns true iff such a variable could be renamed. Else, there was no such variable.

val configure_set : Support.Format.formatter -> (t -> subgoal_hook) list -> Conf.t list -> Beluga_syntax.Syncom.Id.cid_mutual_group * t list
val is_complete : t -> bool