package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

LogtkUnification and Matching

type scope = LogtkSubsts.scope
type subst = LogtkSubsts.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.view.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