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
[Caml-list] type proofs
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2001-12-08 (02:20)
From: Jacques Garrigue <garrigue@k...>
Subject: Re: [Caml-list] type proofs
From: Charles Martin <joelisp@yahoo.com>

> I have the usual kind of type error:
> Values do not match:
>   val send : ('a, int, 'b) t -> 'a -> int
> is not included in
>   val send : ('a, 'b, 'c) t -> 'a -> int
> Now, this is just the tip of an iceberg that goes very deep.  Does
> anyone have a tool somewhere that will print out a more complete
> type proof?  I could check such a proof over to find the true
> mistake.

You can read your source code in the ocamlbrowser editor, and
typecheck it (compiler menu). Then you will be able to check the type
of any subexpression, which is equivalent to having a proof of the

Not that this works particularly well in your case, since the type error
above is at the module level, and your implementation has been checked
succesfully. I know of no tool to build a partial proof, which would
be needed when type checking is not succesful.

Jacques Garrigue
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr