Theoria.Context (theoria v0.3.0)

Copy Markdown View Source

Typing context for bound variables.

Bindings are stored nearest-binder first. A binding's type is stored relative to the context where the binder was introduced. Lookup weakens the stored type into the 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()