rzk-0.11.0: test/typecheck/cases/happy-data-empty.rzk

#lang rzk-1

-- The empty family: no := at all, and the eliminator is ex falso.
#data empty

#check ind-empty : (C : empty → U) → (v : empty) → C v

#define absurd (C : U) (v : empty) : C
  := rec-empty C v