Theoria.Context (theoria v0.1.0)

Copy Markdown View Source

Typing context for bound variables.

Bindings are stored nearest-binder first. A binding's type is always expressed relative to the full current context.

Summary

Types

binding()
t()

Functions

fetch(context, index)
new()
push(context, name, type)
size(context)

Types

binding()

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

t()

@type t() :: %Theoria.Context{bindings: [binding()]}

Functions

fetch(context, index)

@spec fetch(t(), non_neg_integer()) :: {:ok, binding()} | :error

new()

@spec new() :: t()

push(context, name, type)

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

size(context)

@spec size(t()) :: non_neg_integer()