[Agda] importing syntax declarations

[Jean-Philippe Bernardy]

Syntax extensions behave like "infix" declarations. Therefore, if you
import the symbol on which they are defined you'll get them.

Cheers,
JP.

On Thu, Nov 25, 2010 at 1:03 PM, Benedict Kavanagh
<b.i.kavanagh at sms.ed.ac.uk> wrote:
> Hi,
>
> I recently upgraded to 2.2.8. I am experimenting with the NotSoFresh Agda
> development by Pouillard/Pottier,
> http://nicolaspouillard.fr/publis/pouillard-pottier-fresh-look-agda-2010/
> which uses the _:_ operator from Function.agda.
>
> In file NotSoFresh/Lemmas.agda
> ----
> .
> .
> open import Function using (_∘_;_∶_)
> .
> .
> ----
>
> In Agda 2.2.8 the '_:_' operator for adding types to subexpressions is now a
> syntax declaration.
> The above import complains that Function.agda does not export '_:_'.
>
> Can anyone explain how syntax extensions interact with modules?
> In particular can you hide them? Can you selectively import them?
> If so is there a new agda syntax for importing syntax extensions?
>
> Thanks,
> -Ben
>
>
>
>
> --
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>