happy-meta-prefix-option-off.rzk

#lang rzk-1

-- Exercise standalone diagnostics independently of the safe-mode bundle.
#set-option "rstt-safe" = "off"

#set-option "warn-meta-prefix" = "off"

#define my-id (X : U) (x : X) : X := x

-- Would warn at the default (strict) sensitivity; the option disables
-- the check for the rest of the module.
#define stash : Σ (h : (X : U) → X → X), Unit := (my-id, unit)