Module Unif

module Unif: sig .. end

type subst = Substs.t 

type 'a sequence = ('a -> unit) -> unit 

exception Fail

val occurs_check : depth:int ->
       subst -> InnerTerm.t HVar.t Scoped.t -> InnerTerm.t Scoped.t -> bool

Signatures

module type S = Unif_intf.S

Base (scoped terms)

module Inner: S  with type term = InnerTerm.t and type ty = InnerTerm.t

Specializations

module Ty: S  with type term = Type.t and type ty = Type.t

module FO: S  with type term = FOTerm.t and type ty = Type.t