[Agda] hiding implementation

Sergei Meshveliani mechvel at botik.ru
Tue Aug 12 14:36:13 CEST 2014


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





More information about the Agda mailing list