search

argumentcomputer / yatima

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

Replace erased partial functions with their `_unsafe_rec` counterparts #194

Closed winston-h-zhang closed 2 years ago

winston-h-zhang commented 2 years ago

Relevant Zulip thread: https://zulip.yatima.io/#narrow/stream/18-lang/topic/.60_unsafe_rec.60.20strikes.20back