[Why3-club] Coq driver
jean-jacques.levy at inria.fr
Mon Mar 17 08:52:10 CET 2014
Dear Why3 fans,
it looks we have problem with Coq driver in new Why3 0.83:
1- /usr/local/share/why3/drivers/coq.drv exists, but Why3ide seems call
That can be fixed with a link between these 2 filenames.
2- we have a type declaration missing the Coq file.
The following why3 type:
type btree =
| Root (list (pair btree int)) btree
| Node (list (pair btree int)) btree
gives in Coq
(* Why3 assumption *)
Inductive btree :=
| Empty : btree
| Root : (list (@pair btree btree_WhyType Z _)) -> btree -> btree
| Node : (list (@pair btree btree_WhyType Z _)) -> btree -> btree.
Axiom btree_WhyType : WhyType btree.
Existing Instance btree_WhyType.
which when run gives:
Toplevel input, characters 67-80:
Error: The reference btree_WhyType was not found in the current environment.
Hope this message is not new spam. Many thanks for help.
-JJ + Qia -
More information about the Why3-club