logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . TypedSTerm . UStack
type t

Unification stack, for backtracking purposes

val create : unit -> t
type snapshot

A snapshot of bindings at a given moment

val snapshot : st:t -> snapshot

Save current state

val restore : st:t -> snapshot -> unit

Restore all references to their state at snapshot. Bindings done since are undone.