Module formatting 

Lemma source code formatting.

Formats parsed specs into canonical Lemma source text. Value and constraint formatting is delegated to AsLemmaSource (in parsing::ast), which emits valid, round-trippable Lemma syntax. The regular Display impls on AST types are for human-readable output (error messages, evaluation); they are not used here. This module handles layout: alignment, line wrapping, and section ordering.

Constants

MAX_COLS

Soft line length limit. Longer lines may be wrapped (unless clauses, expressions). Facts and other constructs are not broken if they exceed this.

Functions

format_source

Parse a source string and format it to canonical Lemma source.

format_specs

Format a sequence of parsed specs into canonical Lemma source.