η for pairs #22

New Issue

Closed

opened 2023-07-30 16:03:05 -04:00 by rhi · 0 comments

rhi commented

2023-07-30 16:03:05 -04:00

Owner

current idea: add fst and snd, and, in zero contexts, the reduction rule

 e neutral
──────────────────────────────────────
 case e return z ⇒ B of {(x, y) ⇒ t}
  ⇝
 t[fst e/x, snd e/y] ∷ B[e/z]

runtime-relevant η is still out of reach for the usual qtt reasons

current idea: add `fst` and `snd`, and, _in zero contexts_, the reduction rule ``` e neutral ────────────────────────────────────── case e return z ⇒ B of {(x, y) ⇒ t} ⇝ t[fst e/x, snd e/y] ∷ B[e/z] ``` runtime-relevant η is still out of reach for the usual qtt reasons