IlltypedPattern.agda

module IlltypedPattern where

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

f : (A : Set) -> A -> A
f A zero = zero