Skip to content

Stronger `iNext` that performs arithmetic cancelation

Robbert Krebbers requested to merge robbert/iNext_nat_cancel into master

This is WIP that fixes issue #148 (closed). Some questions:

  • Where to put the canceler. Is this something more generic that should be moved to stdpp?
  • Move TCIf to stdpp.
  • How to name MakeIntoLaterN, it's like MakeLaterN, which is used for framing but slightly different, e.g. it does not turn ▷ True into True, but turns ▷^0 P into P and ▷^1 P into ▷ P.
Edited by Robbert Krebbers

Merge request reports