logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . 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
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