Frédéric Blanqui comments

Results 259 comments of


                                            Frédéric Blanqui

Set up GitHub pages to browse the source code documentation online

Shouldn't we rename this issue into "Set up GitHub to browse the source doc online"?

Set up GitHub pages to browse the source code documentation online

But what about the doc of the sources (with ocamldoc)?

Term transformation helper function

@gabrielhdt How do you plan to introduce in LP the rules you want to use? If I remember well, dkmeta takes as argument some file f_in.dk and some set of...

Term transformation helper function

Gabriel, do you want to rewrite dk files only, or lp files also? If you want to rewrite dk files only, there is something easy to do now that lambdapi...

Error in HRS output

This artificially creates non-linear rules.

Declare injectivity on some arguments only

Thanks @Gaspi for your issue. Last week-end, I was thinking in submitting very soon a new PR allowing users to specify in which arguments a symbol is injective. I prefer...

Declare injectivity on some arguments only

Your example works if you declare Term as injective. For the moment, we cannot declare injectivity on specific arguments.

Declare injectivity on some arguments only

A possible workaround is to declare a unification rule.

Error in HRS output

Fixed in #871

Hierarchy of tests

I'm closing this PR because it is too old now.