Reservoir

pnwamk/lean4-assert-command

A simple assertion command for Lean4

GitHub Link Documentation

Pick a version!

TODO: should show a time axes that allows the users to view, filter and click copy the lakefile config.

README

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.