Agda-2.3.2.2: test/succeed/local.agda

module local where

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

infixr 15 _::_

data List (A : Set) : Set where
  nil  : List A
  _::_ : A -> List A -> List A

reverse : {A : Set} -> List A -> List A
reverse {A} xs = rev xs nil
  where
    rev : List A -> List A -> List A
    rev  nil      ys = ys
    rev (x :: xs) ys = rev xs (x :: ys)

postulate
  xs : List Nat