warn-rstt-escape-tope-family.rzk

#lang rzk-1

-- Audit S2 alone: report the introduction, not an unfolded use site.
#set-option "rstt-safe" = "off"
#set-option "warn-free-standing-restriction" = "yes"
#def family (A : U) (a : A) : 2 → U := \ t → A [t === 0_2 ↦ a]