happy-data-empty.rzk

#lang rzk-1

-- Exercise standalone diagnostics independently of the safe-mode bundle.
#set-option "rstt-safe" = "off"

-- 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