rzk-0.11.1: test/typecheck/cases/ill-data-eliminator-duplicate.rzk

#lang rzk-1

-- At most one clause per generated eliminator.
#data d := c
  eliminate with ind-d : (C : d → U) → C c → (x : d) → C x
  eliminate with ind-d : (C : d → U) → C c → (x : d) → C x