WithScopeError.agda

-- There was a bug when scope checking with clauses.
module WithScopeError where

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

f : Nat -> Nat
f n with y
  where y = suc n
f n | x = y x