Module lean_export 

Lean 4 exporter for the typed RML fragment (issue #60).

The exporter translates declaration syntax into a Lean-checkable artifact and rejects probabilistic forms instead of assigning them a Lean meaning.

Structs

LeanExportResult

Structured result returned by export_lean.

Functions

export_lean

Export the supported typed RML fragment to Lean 4 source.

lean_ident

Convert an RML identifier to a Lean-safe identifier.