lean4-assert-command
A simple assertion command for Lean4.
Usage
Assert standard boolean (BEq
) equality by using #assert TERM == TERM
:
Assert equality with a custom predicate using #assert TERM == TERM via PRED
:
Failed assertions are highlighted and show actual and expected values: