Theoria.Equation.Schema.Equation (theoria v0.5.0)

Copy Markdown View Source

One schematic equation theorem generated for a compiled definition.

Summary

Types

binder()
t()

Types

binder()

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

t()

@type t() :: %Theoria.Equation.Schema.Equation{
  binders: [binder()],
  equality_type: Theoria.Term.t(),
  left: Theoria.Term.t(),
  right: Theoria.Term.t(),
  suffix: atom()
}