Module `Logtk`Source

Sourcemodule AllocCache : sig ... end

Sourcemodule Binder : sig ... end

Sourcemodule Builtin : sig ... end

Sourcemodule Cnf : sig ... end

Sourcemodule Comparison : sig ... end

Sourcemodule Compute_prec : sig ... end

Sourcemodule Congruence : sig ... end

Sourcemodule Congruence_intf : sig ... end

The congruence stores a finite representation of a set of (ground) equations an inequalities. It is backtrackable, ie one can go back to a previous point as long as it is compatible with a LIFO usage.

Sourcemodule DBEnv : sig ... end

Sourcemodule Defined_pos : sig ... end

Sourcemodule Dtree : sig ... end

Sourcemodule FV_tree : sig ... end

Sourcemodule FeatureVector : sig ... end

Sourcemodule Fingerprint : sig ... end

Sourcemodule FixpointUnif : sig ... end

Sourcemodule Flex_state : sig ... end

Sourcemodule HO_unif : sig ... end

Sourcemodule HVar : sig ... end

Sourcemodule Hash : sig ... end

Sourcemodule Hashcons : sig ... end

Sourcemodule IArray : sig ... end

Sourcemodule ID : sig ... end

Sourcemodule Ind_ty : sig ... end

Sourcemodule Index : sig ... end

Sourcemodule Index_intf : sig ... end

Sourcemodule InnerTerm : sig ... end

Sourcemodule Input_format : sig ... end

Sourcemodule Int_lit : sig ... end

Sourcemodule Interfaces : sig ... end

Sourcemodule JPFull : sig ... end

Sourcemodule JP_unif : sig ... end

Sourcemodule Lambda : sig ... end

Sourcemodule LazyList : sig ... end

Sourcemodule Literal : sig ... end

Sourcemodule Literals : sig ... end

Sourcemodule Monome : sig ... end

Sourcemodule Multiset : sig ... end

Sourcemodule Multiset_intf : sig ... end

Sourcemodule Multisets : sig ... end

Sourcemodule NPDtree : sig ... end

Sourcemodule Options : sig ... end

Sourcemodule Ordering : sig ... end

Sourcemodule Ordinal : sig ... end

Sourcemodule Output_format : sig ... end

Sourcemodule PUnif : sig ... end

Sourcemodule ParseLocation : sig ... end

Sourcemodule PatternUnif : sig ... end

Sourcemodule Position : sig ... end

Sourcemodule PragUnifParams : sig ... end

Sourcemodule Precedence : sig ... end

Sourcemodule Proof : sig ... end

Sourcemodule Rat_lit : sig ... end

Sourcemodule Rewrite : sig ... end

Sourcemodule SLiteral : sig ... end

Sourcemodule STerm : sig ... end

Sourcemodule Scoped : sig ... end

Sourcemodule Signal : sig ... end

Sourcemodule Signature : sig ... end

Sourcemodule Skolem : sig ... end

Sourcemodule SolidSubsumption : sig ... end

Sourcemodule SolidUnif : sig ... end

Sourcemodule Statement : sig ... end

Sourcemodule Subst : sig ... end

Sourcemodule Term : sig ... end

Sourcemodule Test_prop : sig ... end

Sourcemodule Type : sig ... end

Sourcemodule TypeInference : sig ... end

Sourcemodule TypedSTerm : sig ... end

Sourcemodule Unif : sig ... end

Sourcemodule UnifFramework : sig ... end

Sourcemodule Unif_constr : sig ... end

Sourcemodule Unif_intf : sig ... end

Sourcemodule Unif_subst : sig ... end

Sourcemodule UnionFind : sig ... end

Sourcemodule UntypedAST : sig ... end

Sourcemodule Util : sig ... end

Sourcemodule Var : sig ... end

package logtk

Module LogtkSource

Module `Logtk`Source