type t = resulttype 'a tc = 'a result_tctype inst_subst = (term, term) Var.Subst.tA 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 ->
?flavor:('a -> flavor) ->
unit ->
'a tcMake a result typeclass, for considering values of type 'a as proof results.
print in given syntax
true only if 'a is a toplevel statement (default false)
returns the name of the result. Typically, a name from the input file
apply substitution, then convert to form. If not provided, will fail.
include Interfaces.ORD with type t := tinclude Interfaces.EQ with type t := tval pp_in : Output_format.t -> t CCFormat.printerval pp : t CCFormat.printerval is_stmt : t -> boolval to_form : ?ctx:Term.Conv.ctx -> t -> formval to_form_subst :
?ctx:Term.Conv.ctx ->
Subst.Projection.t ->
t ->
form * inst_substinstantiated form + bindings for vars
val name : t -> string option