packages feed

rzk-0.11.1: test/typecheck/cases/ill-data-path-indexed.rzk

#lang rzk-1

-- Path constructors in indexed families are not supported yet.
#data bad (A : U) : A → U
  := mk (a : A) : bad A a
   | pth (a : A) : mk A a =_{bad A a} mk A a