Version française
Home     About     Download     Resources     Contact us    
Browse thread
prefix ::
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Damien Doligez <damien.doligez@i...>
Subject: Re: [Caml-list] prefix ::
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