search

argumentcomputer / yatima

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

Double check `Yatima.Expr.isVarFree` and `Yatima.Expr.getBVars` #164

Closed arthurpaulino closed 2 years ago

arthurpaulino commented 2 years ago

I was expecting getBVars to get the names of lam/pi/letE binders, but it's doing something else

arthurpaulino commented 2 years ago

This is low priority. isVarFree is used for debugging and getBVars is not used at all