Re: [Why3-club] Get TPTP from Why3

2017-05-10 Thread Claude Marché
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

[Why3-club] Get TPTP from Why3

2017-05-10 Thread Antoine DEFOURNE
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é