why3_tptp.drv 503 Bytes
Newer Older
1 2
(* Why driver for Why3 syntax *)

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

6 7
transformation "inline_trivial"

8
transformation "eliminate_builtin"
9 10 11
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
12
transformation "eliminate_literal"
13
transformation "eliminate_epsilon"
14 15
transformation "eliminate_if"
transformation "eliminate_let"
16

17
transformation "discriminate"
18
transformation "encoding_tptp"
19 20

theory BuiltIn
21
  syntax predicate (=)  "(%1 = %2)"
22
end