rzk-0.11.4: test/typecheck/cases/ill-rstt-meta-prefix.rzk
#lang rzk-1 #set-option "rstt-safe" = "error" #set-option "warn-meta-prefix" = "off" #def my-id (X : U) (x : X) : X := x #def stash : Σ (h : (X : U) → X → X), Unit := (my-id, unit)
#lang rzk-1 #set-option "rstt-safe" = "error" #set-option "warn-meta-prefix" = "off" #def my-id (X : U) (x : X) : X := x #def stash : Σ (h : (X : U) → X → X), Unit := (my-id, unit)