lean4-assert-command

A simple assertion command for Lean4.

Usage

Assert standard boolean (BEq) equality by using #assert TERM == TERM:

Passing assertions are underlined in green and report success.

Assert equality with a custom predicate using #assert TERM == TERM via PRED:

Passing assertions with custom equality are underlined in green and report the success and custom equality function.

Failed assertions are highlighted and show actual and expected values:

Failed assertions are underlined in red and report the terms' values.