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:
