warn-rstt-default.rzk

#lang rzk-1

-- RSTT-safe mode is off by default: the schematic binder inside the body
-- passes silently.
#set-option "warn-meta-binder" = "no"
#set-option "warn-meta-prefix" = "off"
#def nested (A : U) (a : A) : A
  := (\ (B : U) (b : B) → b) A a