happy-tope-rec-and-restrict.rzk

#lang rzk-1

-- `recOR` with a disjunctive shape so `contextEntailsUnion` is satisfied: the context is
-- covered by the union of branch guards.
#define u : U := Unit -> Unit

#define happyRecOrBoundary (t : 2 | (t === 0_2) \/ (t === 1_2)) : U
  := recOR( t === 0_2 |-> u, t === 1_2 |-> u )

-- Contradictory guard: context entails `⊥`, so `recBOT` is well-typed.
#define happyRecBotContradiction (t : 2 | (t === 0_2) /\ (t === 1_2)) : U
  := recBOT

-- Trivial restriction on the `TOP` face: typechecks (the restriction holds everywhere).
#define happyRestrictedUnitTrivial : Unit [ TOP |-> unit ]
  := unit