rzk-0.11.4: test/typecheck/cases/ill-rstt-uncovered-endpoints.rzk
#lang rzk-1 #set-option "rstt-safe" = "error" #def uncovered (A : U) (a : A) (t : 2) : A := recOR (t === 0_2 ↦ a, t === 1_2 ↦ a)
#lang rzk-1 #set-option "rstt-safe" = "error" #def uncovered (A : U) (a : A) (t : 2) : A := recOR (t === 0_2 ↦ a, t === 1_2 ↦ a)