Module Proof.Result

type t = result
type 'a tc = 'a result_tc
type flavor = [
| `Pure_bool
| `Absurd_lits
| `Proof_of_false
| `Vanilla
| `Def
]
type inst_subst = (term, term) Var.Subst.t

A mapping used during instantiation, to map pre-instantiation variables to post-instantiation terms

val make_tc : of_exn:(exn -> 'a option) -> to_exn:('a -> exn) -> compare:('a -> 'a -> int) -> to_form:(ctx:Term.Conv.ctx -> 'a -> form) -> ?⁠to_form_subst:(ctx:Term.Conv.ctx -> Subst.Projection.t -> 'a -> form * inst_subst) -> pp_in:(Output_format.t -> 'a CCFormat.printer) -> ?⁠name:('a -> string) -> ?⁠is_stmt:bool -> ?⁠is_dead_cl:(unit -> bool) -> ?⁠flavor:('a -> flavor) -> unit -> 'a tc

Make a result typeclass, for considering values of type 'a as proof results.

parameter pp_in

print in given syntax

parameter is_stmt

true only if 'a is a toplevel statement (default false)

parameter name

returns the name of the result. Typically, a name from the input file

parameter to_form_subst

apply substitution, then convert to form. If not provided, will fail.

val make : 'a tc -> 'a -> t
val form_tc : form tc
val of_form : form -> t
include Interfaces.ORD with type t := t
type t
val compare : t -> t -> int
include Interfaces.EQ with type t := t
type t
val equal : t -> t -> bool
val pp_in : Output_format.t -> t CCFormat.printer
val pp : t CCFormat.printer
val is_stmt : t -> bool
val is_dead_cl : t -> unit -> bool
val to_form : ?⁠ctx:Term.Conv.ctx -> t -> form
val to_form_subst : ?⁠ctx:Term.Conv.ctx -> Subst.Projection.t -> t -> form * inst_subst

instantiated form + bindings for vars

val flavor : t -> flavor
val name : t -> string option