[Agda] type annotation in-place
Jesper Cockx
Jesper at sikanda.be
Wed Oct 7 14:35:27 CEST 2015
I meant syntax declaration, not a pattern synonym.
Jesper
On Wed, Oct 7, 2015 at 2:34 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
> 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/9afe2feb/attachment.html
More information about the Agda
mailing list