argumentcomputer / yatima

A zero-knowledge Lean4 compiler and kernel
MIT License
114 stars 8 forks source link

Add hashes to `Typechecker.Expr` #185

Closed gabriel-barrett closed 2 years ago

gabriel-barrett commented 2 years ago

We should add the anon cids (and probably meta cids too) to Typechecker.Expr in order to be able to cache results. It also allows us to implement primitive operations like Lean does, but using cids instead of names