Re: [Caml-list] Agda-style parser

[Wojciech Meyer <wojciech.meyer@googlemail.com>]

Hi,

I think his talking about "mix-fix" notation.

Basically the underscores are placeholders for expression in "mix-fix"
operator that can be subsitutied by any expression:

if _ then _ else _ = fun cond yes no -> if cond then yes else no

please note that under strict evaulation like in OCaml it will not be correct.

Another example:

_ ++ _ = List.append

In Coq there is support for mix-fix operators via. Notation.

Wojciech


On Fri, Jul 6, 2012 at 2:17 PM, Fabrice Le Fessant
<Fabrice.Le_fessant@inria.fr> wrote:
> Could you give more details about what you are looking for, for those
> ones who are not familiar with Agda "cool underscore thingy" ?
>
> Thx,
> -Fabrice
>
> On Fri, Jul 6, 2012 at 2:52 PM, Andrej Bauer <andrej.bauer@andrej.com> wrote:
>> If I wanted a parser in Ocaml that can parse things in teh style of
>> Agda (with the cool underscore thingy), where would I start looking?
>>
>> With kind regards,
>>
>> Andrej
>>
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa-roc.inria.fr/wws/info/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>>
>
>
>
> --
> Fabrice LE FESSANT
> Chercheur en Informatique
> INRIA Saclay -- Ile-de-France
> Programming Languages and Distributed Systems
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>