search

argumentcomputer / yatima

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

Caching expressions and universes #172

Closed arthurpaulino closed 2 years ago

arthurpaulino commented 2 years ago

Every universe level and expression was compiled as if it were the first time, adding a lot of overhead due to recomputations.

This PR adds caching to the compilation of those objects, cutting out the overhead by the cost of searches on RBMaps.

Closes #170