rzk-0.11.4: test/typecheck/cases/ill-rstt-postulate.rzk
#lang rzk-1 #set-option "rstt-safe" = "error" #postulate restricted (A : U) (a : A) : A [TOP ↦ a]
#lang rzk-1 #set-option "rstt-safe" = "error" #postulate restricted (A : U) (a : A) : A [TOP ↦ a]