[Agda] type annotation in-place
Jesper Cockx
Jesper at sikanda.be
Wed Oct 7 14:34:39 CEST 2015
I'm not sure if I understand. With _∋_, you could write
foo123foo = Foo ∋ foo'
>
> foo = Foo ∋ foo' (T ∋ f x) y
>
You could also use a pattern synonym to put the type signature after the
term instead of before:
El : ∀ {a} (A : Set a) → A → A
> El A x = x
>
> syntax El A x = x ∈ A
>
> foo123foo = foo' ∈ Foo
>
> foo = foo' (f x ∈ T) y ∈ Foo
>
On Wed, Oct 7, 2015 at 2:01 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> On Wed, 2015-10-07 at 13:54 +0200, Jesper Cockx wrote:
> > From Function.agda in the standard library:
> >
> > -- In Agda you cannot annotate every subexpression with a type
> > -- signature. This function can be used instead.
> >
> > _∋_ : ∀ {a} (A : Set a) → A → A
> > A ∋ x = x
> >
> >
> > Does this solve your problem?
> >
>
> No. I meant the implementation part -- the part after `` = ''.
>
> ------
> Sergei
>
>
>
>
> > On Wed, Oct 7, 2015 at 1:41 PM, Sergei Meshveliani <mechvel at botik.ru>
> > wrote:
> > Is it possible to allow in Language the syntax like
> >
> > foo123foo = foo' : Foo
> >
> > (instead of
> > foo123foo : Foo
> > foo123foo = foo'
> > )
> > ?
> >
> > And one also could think of expressions like
> >
> > foo = foo' (f x : T) y : Foo
> >
> > This will make programs a bit more readable.
> >
> > Regards,
> >
> > ------
> > Sergei
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> >
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151007/7c2a0143/attachment.html
More information about the Agda
mailing list