search

argumentcomputer / yatima

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

Can't typecheck `add_comm` #263

Closed arthurpaulino closed 1 year ago

arthurpaulino commented 1 year ago

Do the following commands to reproduce it:

$ lake exe yatima ca Fixtures/Debug/AddComm.lean -e add_comm.env
$ lake exe yatima prove add_comm -e add_comm.env --no-hash -r