Closed arthurpaulino closed 1 year ago
Adding an option to generate Lurk code with reused and more compact variable names, resulting on a source that can be hashed significantly faster.
This should also avoid some reader errors from lurkrs.
lurkrs
lake exe yatima gen Fixtures/CodeGeneration/TCFunctions.lean -d runCheckStore -r -a works correctly, but passing -rs instead doesn't work.
lake exe yatima gen Fixtures/CodeGeneration/TCFunctions.lean -d runCheckStore -r -a
-rs
Adding an option to generate Lurk code with reused and more compact variable names, resulting on a source that can be hashed significantly faster.
This should also avoid some reader errors from
lurkrs.lake exe yatima gen Fixtures/CodeGeneration/TCFunctions.lean -d runCheckStore -r -aworks correctly, but passing-rsinstead doesn't work.