Toolchain support

Checkout full help by running ndpc --help

Formatting

Run

ndpc format proof.ndp

The formatter is an uncompromising formatter, meaning that it will not respect what you wrote, it will only format it in the way that it sees fit.

Compiling to HTML

Run

ndpc compile --html proof.ndp

This will generate proof.html. You can style it however you want by passing --css [FILE]. Read the generated HTML to see the specific selectors involved.

Example output

(you may have to reload if you see a 404)

Compiling to Latex

ndpc compile --latex proof.ndp

The generated output uses boxproof, make sure you follow the installation instructions there.

Compiling to Typst

ndpc compile --typst proof.ndp

The relevant library is maintained here.

Compiling to Lean

ndp proofs can be compiled to lean for formal verification.

ndpc compile --lean proof.ndp
lean proof.lean