Nouvelle syntaxe pour écrire des records (co)inductifs :

CoInductive stream (A:Type) := { hd : A ; tl : stream A }.

Inductive nelist (A:Type) := { hd : A ; tl : option (nelist A) }.

L'affichage n'est pas encore poli. Il reste à choisir l'exact destin de 
la syntaxe qui était apparue dans la 8.2beta pour les records 
coinductifs (qui consistait à utiliser "Record" au lieu de "CoInductive" 
comme maintenant).
VernacRecord et VernacInductive semblent maintenant faire doublon, il 
doit y avoir moyen de les fusionner.
Les records mutuellement inductifs restent aussi à faire.





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11539 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions