Add proof irrelevance - Githubissues

argumentcomputer / yatima

A zero-knowledge Lean4 compiler and kernel

MIT License

121 stars 9 forks source link

Closed arthurpaulino closed 2 years ago

arthurpaulino commented 2 years ago

Closes #188

arthurpaulino commented 2 years ago

Does it work if we uncomment the extractor in Tests/Termination/Prelude.lean? 👀