search

argumentcomputer / yatima

A zero-knowledge Lean4 compiler and kernel
MIT License
121 stars 9 forks source link

Add a `--no-hash` flag to `prove` #265

Closed arthurpaulino closed 1 year ago

arthurpaulino commented 1 year ago

With this flag we should be able to debug the compiled typechecker more efficently. If this flag is set, prove should output the respective data store and a Lurk file that looks like this:

(<typechecker code, which is a lambda> <constant hash>)