PatternShadowsConstructor.agda

module PatternShadowsConstructor where

module A where

  data B : Set where
    x : B

  data C : Set where
    c : B → C

open A using (C; c)

f : C → C
f (c x) = x