Theoria.Lean.Encodable protocol (theoria v0.3.0)

Copy Markdown View Source

Experimental/internal API for 0.2; subject to change before 0.3. Protocol for rendering Theoria structures as Lean oracle source.

Summary

Types

t()

All the types that implement this protocol.

Functions

encode(value, context)

Encodes a value as Lean source with a de Bruijn context.

Types

t()

@type t() :: term()

All the types that implement this protocol.

Functions

encode(value, context)

@spec encode(t(), [String.t()]) :: String.t()

Encodes a value as Lean source with a de Bruijn context.