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 constraints
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2004-12-09 (03:07)
From: skaller <skaller@u...>
Subject: Re: [Caml-list] Type constraints
On Thu, 2004-12-09 at 01:23, Jacques Garrigue wrote:

> Yet, modules are strange beasts for typing, so I wouldn't add the code
> before thinking it through.

I am curious as to the status of COQ support for verifying
assertions about proposed changes to the type system.

For example supposing you did 'think it through' and it
seemed right, would you be able to then extend an
existing COQ proof and attempt to prove your thinking

John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net