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 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,
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language