Theoria.Equation.Matcher.Statement.Frame (theoria v0.3.0)

Copy Markdown View Source

Internal binder frame for matcher equation statement planning.

Summary

Types

binder()
t()

Functions

binders(frame)
fetch(frame, name)
forall(frame, body)
new(binders)
push(frame, name, type)
push_many(frame, binders)
ref(frame, name)
ref!(frame, name)

Types

binder()

@type binder() :: {atom(), Theoria.Term.t()}

t()

@type t() :: %Theoria.Equation.Matcher.Statement.Frame{binders: [binder()]}

Functions

binders(frame)

@spec binders(t()) :: [binder()]

fetch(frame, name)

@spec fetch(t(), atom()) :: {:ok, {binder(), non_neg_integer()}} | {:error, term()}

forall(frame, body)

@spec forall(t(), Theoria.Term.t()) :: Theoria.Term.t()

new(binders)

@spec new([binder()]) :: t()

push(frame, name, type)

@spec push(t(), atom(), Theoria.Term.t()) :: t()

push_many(frame, binders)

@spec push_many(t(), [binder()]) :: t()

ref(frame, name)

@spec ref(t(), atom()) :: {:ok, Theoria.Term.BVar.t()} | {:error, term()}

ref!(frame, name)

@spec ref!(t(), atom()) :: Theoria.Term.BVar.t()