registerUnliftFinisher
Registers a new finisher function for constructing the final proof of equality after unlifting inner expressions. The function should take the original left-hand side and right-hand side, the transformed left-hand side and right-hand side, the common universe level, and return a proof of equality.
Code
def registerUnliftFinisher (f : finisherMetadata) : IO Unit := do
unliftFinisherRef.modify (·.push f)Actions: Source · Open Issue
Meaning last changed in v4.34.0-rc2-1-g439785b (2026-08-23).
Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.
Dependency graph
Audit surface: 1 project declarations, 17 external constants
✓ Proved: no sorry anywhere in its closure
This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.