3.2. Two parser registries🔗

External parser libraries are normalized through two extensible attributes:

• @[triptych_parser] contains terminating successful-path simplification rules;

• @[triptych_parser_search =] contains equality or equivalence facts suitable for bounded E-matching.

Decimal registers its successful-parser characterization in both:

Its source declaration begins with @[triptych_parser, triptych_parser_search =] theorem parse_eq_some_iff_parts.

The first attribute gives simp a directed rewrite from parser success to the component facts. The = in triptych_parser_search = is not assignment syntax: it registers the theorem as an equality or equivalence rule for grind's E-matching, which may use it in either direction.

triptych_sound [defs] at h uses the first registry. In Decimal's Decimal.RuleRegistrySoundness.parser_agrees proof, this one line replaces a raw Cedar parser equation with the sign, natural-part, fraction-part, and range witnesses proved by Decimal.RuleRegistryProof.parse_eq_some_iff_parts:

Without the registration, that proof would have to invoke the long Decimal.RuleRegistryProof.parse_eq_some_iff_parts theorem explicitly at every use site. The theorem's parser analysis is proved once in RuleRegistryProof.lean; later proofs consume only its grammar-shaped result.

The second registration matters when proof search needs the equivalence in the other direction. Here the component facts are enough for grind to recover parser success:

triptych_auto [local] first uses the explicitly supplied definitions or facts, normalizes with the terminating registry, and then runs bounded grind search with the second registry. The bracketed list is local to that invocation; it does not register its contents. When a supplied theorem already rewrites the goal, ordinary simp is the clearer proof.

For example, Datetime's Datetime.RuleRegistryProof.parts_of_parse_eq_some is closed by triptych_auto [datetimeMillis]: the local definition connects the returned Cedar value to epoch milliseconds, while the registries supply the reusable parser decomposition and bounded search. The tactic combines registered facts; it does not invent Datetime semantics.