rzk-0.11.4: test/typecheck/cases/ill-rstt-boundary-obligation.rzk
#lang rzk-1 #set-option "rstt-safe" = "error" #def boundary-obligation (A : U) (a b : A) ((s, t) : 2 * 2 | s === 0_2 /\ t === 0_2) : A [s === t ↦ a] := b
#lang rzk-1 #set-option "rstt-safe" = "error" #def boundary-obligation (A : U) (a b : A) ((s, t) : 2 * 2 | s === 0_2 /\ t === 0_2) : A [s === t ↦ a] := b