[Why3-club] Consistency of map theory

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Thu Nov 22 20:17:28 CET 2012


> I still wonder: wouldn't it be a good idea to prove the lemma's in
> why3 theories?

Definitely. We can do it and we should do it.

We already have Coq realizations for several theories from Why3's
standard library (have a look in lib/coq/ subdirectory).

Unfortunately, we haven't done it for all theories, and that includes
theory map.

By the way, I'm the one to be blamed for this inconsistency and I apologize.

Best regards,
-- 
Jean-Christophe



More information about the Why3-club mailing list