Module LogtkUnif

module LogtkUnif: sig .. end

LogtkUnification and Matching

type scope = LogtkSubsts.scope 
type subst = LogtkSubsts.t 
type env = LogtkScopedTerm.t LogtkDBEnv.t 
type 'a sequence = ('a -> unit) -> unit 

Result of (multiple) LogtkUnification

type res = subst sequence 
val res_head : res -> subst option
Obtain the first result, if any
Since 0.5.2
exception Fail
Raised when a unification/matching attempt fails


module type UNARY = sig .. end
module type NARY = sig .. end

Base (scoped terms)

module Nary: NARY  with type term = LogtkScopedTerm.t
module Unary: UNARY  with type term = LogtkScopedTerm.t
To be used only on terms without LogtkScopedTerm.Multiset constructor


module Ty: UNARY  with type term = LogtkType.t
module FO: UNARY  with type term = LogtkFOTerm.t
module HO: NARY  with type term = LogtkHOTerm.t


module Form: sig .. end