[Agda] hiding implementation

[Dominique Devriese]

Sergei,

This may not be an error but just indicative of the fact that the
type-correctness of f depends on the reduction behavior of foo.
Here's a simpler example of this phenomenon:

  open import Data.Product
  open import Relation.Binary.PropositionalEquality

  foo : ∀ {A : Set} → A → A
  foo x = x

  -- postulate foo : ∀ {A : Set} → A → A

  f : ∀ {A} → (x : A) → Σ A (λ y → x ≡ y)
  f x = foo x , refl

You might also be interested in Agda's abstract keyword, which hides
the reduction behavior of a term, although I need to check the details
of how it's used.

Regards,
Dominique

2014-08-12 14:36 GMT+02:00 Sergei Meshveliani <mechvel at botik.ru>:
> People,
>
> there is the following effect in Agda (of July 2014).
> There are some programs of kind
>
>   foo : <signature>
>   foo x =  <implementation>
>
>   -- in another module ----
>   f : <signature2>
>   f y =  ...
>          foo y       -- using  foo
>          ...
>
>
> They are type-checked.
> And if we                      postulate foo : <signature>
> and remove its implementation,
> then Agda reports an error for  f  for the place where  foo  is applied.
>
> Such cases as with  foo and f  are rare, but they present in my
> application.
>
> Is this an error in Agda ?
>
> Regards,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda