Agda-2.3.2.2: test/succeed/PartiallyAppliedConstructorInIndex.agda

module PartiallyAppliedConstructorInIndex where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat
  plus : Nat -> Nat -> Nat

data D : (Nat -> Nat) -> Set where
  c : D suc
  d : (x : Nat) -> D (plus x)
  e : D (\ x -> suc x)
 
f : D suc -> Nat
f c = zero
f e = suc zero