Shari the 🍣 prover

Shari is an interactive theorem prover for writing proofs in the internal language of topos with NNO (intuitionistic higher-order arithmetic).

Try it out online here!