Version française
Home     About     Download     Resources     Contact us    
Browse thread
type generalization of recursive calls
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Stéphane Gimenez <stephane.gimenez@p...>
Subject: Re: type generalization of recursive calls
Hi,

Thanks for your answers. Thanks to Damien for the handy
workarounds and to Boris for the sevral insightful comments.

I'll probably switch to the svn version, waiting for 3.12...

I think 3.13 was a typo, see:
  http://caml.inria.fr/svn/ocaml/trunk/Changes

Stéphane

PS:
btw, looks like coq is not really fond of this data type:

Inductive t a : Type :=
  | E : t a
  | D : t a -> t a -> t a
  | O : a -> t a
  | I : t (t a) -> t a
.

Error: Non strictly positive occurrence of "t" in "t (t a) -> t a".