package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Proof.ResultSource

Sourcetype t = result
Sourcetype 'a tc = 'a result_tc
Sourcetype flavor = [
  1. | `Pure_bool
  2. | `Absurd_lits
  3. | `Proof_of_false
  4. | `Vanilla
  5. | `Def
]
Sourcetype inst_subst = (term, term) Var.Subst.t

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

Sourceval 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 -> ?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.

Sourceval make : 'a tc -> 'a -> t
Sourceval form_tc : form tc
Sourceval of_form : form -> t
include Interfaces.ORD with type t := t
Sourceval compare : t -> t -> int
include Interfaces.EQ with type t := t
Sourceval equal : t -> t -> bool
Sourceval is_stmt : t -> bool
Sourceval to_form : ?ctx:Term.Conv.ctx -> t -> form
Sourceval to_form_subst : ?ctx:Term.Conv.ctx -> Subst.Projection.t -> t -> form * inst_subst

instantiated form + bindings for vars

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