Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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: 2010-02-18 (14:24)
From: Stéphane Gimenez <stephane.gimenez@p...>
Subject: Re: type generalization of recursive calls

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:


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".