warn-meta-binder-inside-term.rzk

#lang rzk-1

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

-- Schematic parameters are bound in a declaration's parameter prefix, so
-- that a declaration is a family of object-theory statements, one per
-- instantiation. A λ inside a term that binds a universe, a cube or a tope
-- family is outside that reading; it is reported when asked for.

#set-option "warn-meta-binder" = "yes"

-- Leading λs are the declaration's own parameters: silent.
#def my-id : (X : U) → X → X
  := \ X x → x

#def at-universe (A : U) (a : A) : A
  := (\ (B : U) → \ (b : B) → b) A a

#def at-cube (A : U) (a : A) : A
  := (\ (J : CUBE) → a) 2

#def at-tope-family (I : CUBE) (A : U) (a : A) : A
  := (\ (φ : I → TOPE) → a) (\ t → TOP)

-- A schema defined by recursion on a schematic index: the case split has to
-- come first, so the remaining parameters are bound in its branches. Both the
-- index and the universe are in the meta prefix, so uses supply them; silent.
#data nat := zero | suc (n : nat)

#def Schematic (n : nat) : U
  := ( A : U) → A → A

#def by-index (n : nat) : Schematic n
  := match n
     ( zero ⇒ \ A a → a
     | suc _ ih ⇒ \ A a → ih (A → A) (\ x → x) a)

-- Supplying a schema at a schematic parameter is the plumbing the
-- meta-prefix check allows; silent.
#def takes-schema (h : (A : U) → A → A) (B : U) (b : B) : B
  := h B b

#def supplies-schema (B : U) (b : B) : B
  := takes-schema (\ A a → a) B b