-
Notifications
You must be signed in to change notification settings - Fork 0
Open
Description
Just a heads-up, the MMB format has changed to eliminate ConvRef
. Ref
should pop a conversion obligation if the heap element is a conversion.
Lines 179 to 182 in 491ab31
fn reference(&mut self, idx: u32) -> KResult { | |
let i = self.proof_heap.get(idx).ok_or(Kind::InvalidHeapIndex)?; | |
self.proof_stack.push(i); |
Unfold
also no longer pops three elements from the stack. See https://github.com/digama0/mm0/blob/master/mm0-c/mmb.md
Metadata
Metadata
Assignees
Labels
No labels