why3.drv 366 Bytes
Newer Older
1 2
(* Why driver for Why3 syntax *)

3
printer "why3"
4
filename "%f-%t-%g.why"
5

6 7
(* transformation "detect_polymorphism" *)

8
theory BuiltIn
9 10
  syntax type  int  "int"
  syntax type  real "real"
11
  syntax predicate (=)  "(%1 = %2)"
12
  (* meta "encoding:ignore_polymorphism_ls" predicate (=) *)
13
end
14

15 16 17 18 19
(*
theory list.List
  meta "encoding:ignore_polymorphism_ts" type list
end
*)