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

LogtkSignatures


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

Specializations


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

LogtkFormulas


module Form: sig .. end