Experimental/internal API for 0.2; subject to change before 0.3.
Encodes Theoria core terms as Lean source for contributor oracle checks.
The public API is intentionally small; concrete rendering is dispatched
through Theoria.Lean.Encodable so each core term owns its Lean shape. The
encoder does not prove or simplify anything; Lean remains the external checker
for generated files.
Summary
Functions
Applies a Lean function source to encoded argument sources.
Encodes a Theoria constant name in the Lean oracle namespace.
Returns a binder name that does not collide with the current Lean context.
Encodes an atom as a Lean identifier.
Encodes a universe level as a Lean universe expression.
Wraps Lean source in parentheses.
Encodes a sort level as Prop, Type, Type n, or Sort u.
Encodes a Theoria term as a Lean expression.
Encodes a Theoria term as a Lean expression with a de Bruijn context.
Functions
Applies a Lean function source to encoded argument sources.
Encodes a Theoria constant name in the Lean oracle namespace.
Returns a binder name that does not collide with the current Lean context.
Encodes an atom as a Lean identifier.
@spec level(Theoria.Level.t()) :: String.t()
Encodes a universe level as a Lean universe expression.
Wraps Lean source in parentheses.
@spec sort(Theoria.Level.t()) :: String.t()
Encodes a sort level as Prop, Type, Type n, or Sort u.
@spec term(Theoria.Term.t()) :: String.t()
Encodes a Theoria term as a Lean expression.
@spec term(Theoria.Term.t(), [String.t()]) :: String.t()
Encodes a Theoria term as a Lean expression with a de Bruijn context.