ill-data-tope-index.rzk

#lang rzk-1

-- An index of a #data sort must be a type.
#data OverTopes : TOPE -> U := at-top : OverTopes TOP