package logtk

  1. Overview
  2. Docs

Module Proof.Result

type t = result
type 'a tc = 'a result_tc
type flavor = [
  1. | `Pure_bool
  2. | `Absurd_lits
  3. | `Proof_of_false
  4. | `Vanilla
  5. | `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
val compare : t -> t -> int
include Interfaces.EQ with type t := t
val equal : t -> t -> bool
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