Hello,
You should decide which TPTP format, e.g
why3 prove -D tptp-tff0 file.why
or
why3 prove -D tptp-tff1 file.why
- Claude
Le 10/05/2017 à 11:32, Antoine DEFOURNE a écrit :
> Hello,
>
> I want to get a problem in TPTP format from a task expressed in Why3. Is
> there already a way to do this, either with Why3 or another tool?
> Ideally, I would do this through the API for OCaml, but I will take
> anything. Thanks in advance.
>
> Antoine Defourné
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex|
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
