rzk-0.11.0: test/typecheck/cases/ill-data-index-mismatch.rzk
#lang rzk-1 #data nat := zero | suc (n : nat) -- the index term must have the index's type (nat is a type, not a nat) #data bad : nat → U := c : bad nat
#lang rzk-1 #data nat := zero | suc (n : nat) -- the index term must have the index's type (nat is a type, not a nat) #data bad : nat → U := c : bad nat