[Agda] Unification assumes injective postulates?

[Nils Anders Danielsson]

On 2012-11-16 16:53, Jan Malakhovski wrote:
> It looks that
> ~~~~
> postulate foo : ℕ → ℕ
>
> bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)
> bar refl = {!!}
> ~~~~
>
> and
>
> ~~~~
> module Postulate (foo : ℕ → ℕ) where
>    bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)
>    bar refl = {!!}
> ~~~~
> work the same way.

Postulates and parameters are not always treated in the same way (unless
things have changed):

   http://code.google.com/p/agda/issues/detail?id=170.

-- 
/NAD