1
module LateMetaVariableInstantiation where
7
{-# BUILTIN NATURAL ℕ #-}
8
{-# BUILTIN ZERO zero #-}
9
{-# BUILTIN SUC suc #-}
12
yippie : (A : Set) → A
14
slow : (A : Set) → ℕ → A
15
slow A zero = yippie A
16
slow A (suc n) = slow _ n
18
data _≡_ {A : Set} (x : A) : A → Set where
21
foo : slow ℕ 1000 ≡ yippie ℕ