lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

fix: unbox init declarations in interpreter

Open digama0 opened this issue 2 years ago • 0 comments

There was an ABI mismatch between the storage of @[init] declarations and the load in the interpreter, leading to garbage results. Discussed on Zulip.

digama0 avatar May 26 '23 08:05 digama0