Custom override for `Std.RBMap`

argumentcomputer / yatima

A zero-knowledge Lean4 compiler and kernel

MIT License

124 stars 9 forks source link

Custom override for `Std.RBMap` #264

Closed arthurpaulino closed 1 year ago

arthurpaulino commented 1 year ago

We should be able to provide a custom Lurk implementation for the Std.RBMap API by using CONS. This implementation should have much less overhead than the compiled version from Lean.

This issue shouldn't be worked on before #263 is solved because we would risk hiding a bug with an override.