rzk-0.11.4: test/typecheck/cases/ill-rstt-restriction.rzk
#lang rzk-1 #set-option "rstt-safe" = "error" #set-option "warn-free-standing-restriction" = "no" #def assumed (A : U) (a : A) (f : (A [TOP ↦ a]) → A) : A := f a
#lang rzk-1 #set-option "rstt-safe" = "error" #set-option "warn-free-standing-restriction" = "no" #def assumed (A : U) (a : A) (f : (A [TOP ↦ a]) → A) : A := f a