ill-data-shape-index.rzk

#lang rzk-1

-- The inline spelling of a shape index is rejected on the surface form.
-- The named spelling `#data Fam : D1 → U` for `D1 : 2 → TOPE` is rejected
-- too, on the elaborated sort (see ill-data-shape-index-named), so the two
-- spellings of one thing meet the same rule.
#data Fam : (t : 2 | ⊤) → U
  := at (t : 2 | ⊤) : Fam t