@hackage / ivor

Theorem proving library based on dependent type theory