Skip to content

Change recursive domain to `proto = 1 + (action * ▶ (V → proto → PROP))`.

Robbert Krebbers requested to merge robbert/kill_laters into master

By moving the later further to the outside, we can kill many occurences of Next, and get rid of laters/except_0s at awkward positions. Also we can have a sensible eliminator proto_elim.

Edited by Robbert Krebbers

Merge request reports