Frédéric Blanqui

Hi @ejgallego ! It's good to hear from you. I hope every thing will be all right for you. For your information, Amélie started a M2 internship about one month...

The current code for exporting HRS is buggy. Please use https://github.com/Deducteam/lambdapi/pull/871 instead. It should be merged into master very soon. By the way, did you succeed in compiling CSI^ho or...

Well, README says to use OCaml 3.12 (very old!). But I get the following error: ``` In file included from gpw/glueminisat/core/Solver.h:28, from gpw/Solver.h:25, from gpw/PbSolver.h:24, from gpw/PbParser.h:23, from gpw/PbParser.C:20: gpw/glueminisat/core/SolverTypes.h:50:16:...

The output is now: ``` (FUN A : t -> t -> t L : t -> (t -> t) -> t P : t -> (t -> t) ->...

Side remarks: Remark 1: the generated code in your last comments and targz file does not seem up to date (there should be no m_typ in the output). But this...

Right, AC and non-nullary pattern variables are a current limitation of LP only. The HRS export should be correct but AC is not part of the HRS format, is it?...

Using the export command, I get: ``` (FUN A : t -> t -> t L : t -> (t -> t) -> t P : t -> (t ->...

As you can see, higher-order pattern variables are translated as you suggested. If you give this system (after some simple renamings) to the web interface of CSI^ho, you get: ```...

After some renamings, the critical pair is: ``` A (A union (A (A union (A (A bind x) (L y))) (A (A bind z) (L y)))) (A (A union (A...

I got this message from Fabian Mitterwallner @fabeulous but didn't have the time to test it yet: ``` Dear Frédéric, I believe CSI^ho is unfortunately no longer maintained. However, since...