2.6 Tracing §2.5: if/then/else, both branches
The Verse Calculus has no boolean type or conditional. Instead if e then e2 else e3 desugars to one{(one{e; e2}) | e3}. The inner one{e; e2} runs the condition and, on success, continues to the then-payload; on failure it yields fail. The outer one then commits to the first surviving alternative of fail | e3 — selecting the then-result on success, or routing to e3 on failure. So fail and choose give else for free.
The true branch: condition 1=1, then 10, else 20. Result: 10.
The false branch: condition 1=2, then 10, else 20. Result: 20.
2.6.1 The true branch
2.6.1.1 Step 1 — U-LIT
The condition 1=1 equates two identical literals, so U-LIT consumes it and the sequence continues to its payload 10. (With different literals this same position would fail — see the false branch.)
2.6.1.2 Step 2 — ONE-VALUE
ONE-VALUE unwraps the inner one{10} to 10, exposing it as the left alternative of the outer choice.
2.6.1.3 Step 3 — ONE-CHOICE
The outer one sees 10 | 20 with a value on the left, so ONE-CHOICE commits to 10 and discards 20 unevaluated — this commitment is what makes if/then/else deterministic.
2.6.2 The false branch
2.6.2.1 Step 1 — U-FAIL
The condition 1=2 equates two different literals; hnf-clash? detects the clash and U-FAIL rewrites the whole sequence 1=2; 10 to fail, wiping out the then-payload.
2.6.2.2 Step 2 — ONE-FAIL
ONE-FAIL propagates the failure out of the inner wrapper: one{fail} reduces to fail.
2.6.2.3 Step 3 — CHOOSE-R
CHOOSE-R reduces fail | e3 to e3: the failed left alternative is discarded, selecting the else-branch.
2.6.2.4 Step 4 — ONE-VALUE
ONE-VALUE unwraps one{20} to 20.
