issues
search
argumentcomputer
/
yatima
A zero-knowledge Lean4 compiler and kernel
MIT License
121
stars
9
forks
source link
Typechecker Fixes
#212
Closed
rish987
closed
1 year ago
rish987
commented
1 year ago
The prelude is typechecking again!
Small bug fixes (the anon hash for
Nat.decLt
changed for some reason)
Small refactor to reorder
recrCtx
mutual constants in mutual inductive blocks to avoid infinite looping while typechecking
The prelude is typechecking again!
Nat.decLtchanged for some reason)recrCtxmutual constants in mutual inductive blocks to avoid infinite looping while typechecking