ADV-050 · evidence animation · formal

Cristian Guerra · QA Automation · Medellín, Colombia · @criguex

Proof-value typecheck control

One proof-value mutation is rejected by Lean. nanoda's rejection category is derived from pinned source, not a structured binary result.

0.0 / 20.0 s

How to read this animation: One fixture changes only the exported proof value. Lean records a type mismatch; nanoda's raw status remains pending and rejection is source-derived. No fresh run is implied.

Accessible explanation, equations, and source records


Open the evidence animation gallery · Download standalone HTML