[Why3-club] Consistency of map theory
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
By the way, I'm the one to be blamed for this inconsistency and I apologize.
More information about the Why3-club