* prefix ::
@ 2005-02-06 22:17 David Monniaux
2005-02-16 14:41 ` [Caml-list] " Damien Doligez
0 siblings, 1 reply; 2+ messages in thread
From: David Monniaux @ 2005-02-06 22:17 UTC (permalink / raw)
To: caml-list
Hi,
In order to east the export of Coq programs to Caml, I'd like to be able
to tell Coq that "cons" on list is OCaml's :: operator. Unfortunately,
it is syntactically incorrect to write:
match l with
[] -> foobar
| ::(x,y) -> blabla
This is a little annoying. Is there anything to do about this?
Thanks,
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: [Caml-list] prefix ::
2005-02-06 22:17 prefix :: David Monniaux
@ 2005-02-16 14:41 ` Damien Doligez
0 siblings, 0 replies; 2+ messages in thread
From: Damien Doligez @ 2005-02-16 14:41 UTC (permalink / raw)
To: caml-list
On Feb 6, 2005, at 23:17, David Monniaux wrote:
> In order to east the export of Coq programs to Caml, I'd like to be
> able to tell Coq that "cons" on list is OCaml's :: operator.
> Unfortunately, it is syntactically incorrect to write:
> match l with
> [] -> foobar
> | ::(x,y) -> blabla
>
> This is a little annoying. Is there anything to do about this?
You will be able to do this in 3.09:
Objective Caml version 3.09+dev16 (2005-02-16)
# let x = (::)(1, []);;
val x : int list = [1]
# match x with (::)(_, _) -> true | [] -> false;;
- : bool = true
#
-- Damien
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2005-02-16 14:41 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2005-02-06 22:17 prefix :: David Monniaux
2005-02-16 14:41 ` [Caml-list] " Damien Doligez
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).