mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
12 lines
237 B
Plaintext
12 lines
237 B
Plaintext
(* Why driver for Why3 syntax *)
|
|
|
|
printer "why3"
|
|
filename "%f-%t-%g.why"
|
|
|
|
theory BuiltIn
|
|
syntax type int "int"
|
|
syntax type real "real"
|
|
syntax predicate (=) "(%1 = %2)"
|
|
meta "encoding:ignore_polymorphism_ls" predicate (=)
|
|
end
|