Frédéric Blanqui
Frédéric Blanqui
I see your point. Develop a strategy language for the rewriting engine (RE) is an interesting topic in its own right. But there has been a lot of works on...
Some commands are not explained in README: - `#REQUIRE`: is it mandatory? - `#NAME`: is it still accepted? - `defac` - `defacu`: what does that mean to declare a symbol...
But what ACU implies? Does that mean that matching is modulo ACU?
I see. It would be good to add a comment about this in the code.
In theory, yes. We currently have a translator from Coq to Dk/Coq, the instance of Dedukti with the encoding of Coq logic. See https://github.com/Deducteam/CoqInE . We also have tools to...
Le 06/10/2020 à 16:46, brando90 a écrit : > > Sorry for yet another comment. Would it translate the proofs too or > just the statements? Since isabelle has "two...
Le 06/10/2020 à 14:12, brando90 a écrit : > > Is it possible to do HOLight to HOL using Dedukti? > HOL-Light and HOL both use OpenTheory I believe, which...
Le 06/10/2020 à 14:02, brando90 a écrit : > > In theory, yes. We currently have a translator from Coq to Dk/Coq, > the instance of Dedukti with the encoding...
Le 17/04/2018 à 08:34, Raphaël Cauderlier a écrit : > > I open this issue to discuss conditional rewriting as a possible > feature request because I just heard of...
Hello Raphaël. Why not encoding your interval function as follows? interval x y --> nil if x >= y -->* true interval x y --> cons x (interval (s x)...