Module Eqnrel


module Eqnrel: sig .. end
Convert a set of Moca relations into a set of equations.


Convert a set of Moca relations into a set of equations.
val eqnset_of_rels : Parsetree.generator -> Parsetree.relations -> Equation.EqnSet.t

Convert a single Moca relation into a set of equations.
val eqns_of_rel : Parsetree.generator -> Parsetree.relation -> (Term.term * Term.term) list

Convert a term into a Code.exp.

Convert a rule into a Code.clause.

Completion of a type declaration.

type kb_result =
| Success of (string * Parsetree.type_declaration) list
| Incomplete
| Fail of Equation.EqnSet.t
val completion : int -> (string * Parsetree.type_declaration) list -> kb_result * bool
val get_kb : unit -> bool
val set_kb : unit -> unit
val get_kb_limit : unit -> int
val set_kb_limit : int -> unit