warn-rstt-escape-section.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"
#section assumptions
#assume A : U
#assume a : A
#assume x : A [TOP ↦ a]
#def use uses (a) : A := x
#end assumptions