English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

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