Theoria.Elaborator (theoria v0.3.0)

Copy Markdown View Source

Converts named Theoria.Syntax terms to de Bruijn-indexed Theoria.Term terms.

The elaborator is a convenience layer. It is intentionally untrusted: callers still need to pass elaborated terms through Theoria.Kernel.

Summary

Types

result()

Functions

elaborate(term)
elaborate(arg1, context)
elaborate!(term)

Types

result()

@type result() :: {:ok, Theoria.Term.t()} | {:error, Theoria.Error.t()}

Functions

elaborate(term)

@spec elaborate(Theoria.Syntax.t()) :: result()

elaborate(arg1, context)

@spec elaborate(Theoria.Syntax.t(), [atom()]) :: result()

elaborate!(term)

@spec elaborate!(Theoria.Syntax.t()) :: Theoria.Term.t()