[Agda] hiding implementation

[Mateusz Kowalczyk]

On 08/12/2014 01:36 PM, Sergei Meshveliani wrote:
> 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
> 
> 

As far as I know, not being able to use postulated things outside of the
module they were postulated in is by design, please someone correct me
if I'm wrong.

The recommended approach is to use a parametrised module anyway: in this
case your module would take ‘foo : <signature>’ as a parameter and you'd
simply use that.

-- 
Mateusz K.