Spec

CharPredicates.lean, Grammar.lean, Types.lean, YamlSpec.lean, Token.lean

Type definitions, token types, grammar inductive, spec production predicates.

Config

Config.lean, Limits.lean

Parser limits and configuration presets (strict / default / permissive / unlimited / safe_tags).

Scanner

Document.lean, Indent.lean, NodeProperties.lean, Scalar.lean, Scanner.lean, SimpleKey.lean, State.lean, Whitespace.lean

Character-to-token conversion with full state management. Split into role-named submodules; the umbrella Scanner.lean owns flow-collection indicators and the scanNextToken dispatch / scan / scanLoop main loop.

Parser

Composition.lean, Fuel.lean, State.lean, TokenParser.lean

Token-to-AST recursive descent. Composition.lean owns the user-facing pipeline (parseYaml*, scanAndParse, comment classification); TokenParser.lean keeps the 14-function mutually-recursive block plus parseStream / parseDocument; State.lean holds ParseState + NodeProperties helpers; Fuel.lean factors out the initialFuel := 4*N+4 formula.

Surface

Basic.lean, Combinators.lean, Document.lean, Node.lean, Scalars.lean, Surface.lean

Formal YAML 1.2.2 surface-syntax grammar productions used to state and discharge the acceptance-strictness theorem.

Schema

Api.lean, Deriving.lean, Dump.lean, FromToYaml.lean, Schema.lean, Struct.lean

Core Schema type resolution, structural API (Api.lean), and deriving for round-tripping user types via FromToYaml.lean.

Output

Dump.lean, Emitter.lean

Canonical Emitter.lean, style-aware Dump.lean, and RoundTrip.lean (emit ∘ parse = id properties).

FFI

FFI.lean

C/Python/Rust bindings via @[export]. The companion ffi/, python/, and rust/ directories outside L4YAML/ carry the non-Lean glue.

Proofs

63 modules

Machine-checked theorems for soundness, completeness, progress, and well-formedness.