drivers/why3_tptp.drv

   1 (* Why driver for Why3 syntax *)
   2
   3 printer "why3"
   4 filename "%f-%t-%g.why"
   5
   6 (* Performed introductions depending on whether counterexamples are
   7    requested, as said by the meta "get_counterexmp". When this meta
   8    set, this transformation introduces the model variables that are
   9    still embedded in the goal. When it is not set, it removes all
  10    these unused-ce-related variables, even in the context.  *)
  11 transformation "counterexamples_dependent_intros"
  12
  13 transformation "inline_trivial"
  14
  15 transformation "eliminate_builtin"
  16 transformation "eliminate_definition"
  17 transformation "eliminate_inductive"
  18 transformation "eliminate_if"
  19 transformation "eliminate_epsilon"
  20 transformation "eliminate_algebraic"
  21 transformation "eliminate_literal"
  22 transformation "eliminate_let"
  23
  24 transformation "discriminate"
  25 transformation "encoding_tptp"
  26
  27 theory BuiltIn
  28   syntax predicate (=)  "(%1 = %2)"
  29 end