Module meta 

Structs

MetaDiagnostic

Generic per-check diagnostic produced by the metatheorem checker. We flatten the per-checker diagnostic types (TotalityDiagnostic etc.) into a single shape so the report consumer does not have to know which underlying checker emitted the message.

MetatheoremCheck

One entry in a MetatheoremResult: which sub-check ran, whether it passed, and which diagnostics it emitted on failure.

MetatheoremReport

Top-level structured report returned by check_metatheorems. The CLI uses format_report to render it; library consumers can read the structured fields directly.

MetatheoremResult

Per-relation (or per-definition) outcome — combines every sub-check run for that name.

Enums

CheckKind

Which checker produced this entry. Totality and Coverage are reported per relation; Termination is reported per definition.

Functions

check_metatheorems

Public API: evaluate text, then enumerate every relation that has a (mode ...) declaration plus matching (relation ...) clauses, and every definition that has a (define ...) declaration. Each candidate becomes a metatheorem result.

format_report

Render a MetatheoremReport as the same human-readable text the CLI prints. Useful in tests that want to assert on the rendered output as well as the structured shape.