Frédéric Blanqui
Frédéric Blanqui
Perfect. Thank you.
Thank you for your comment. Yes, it would be great to add this feature. As explained before, for rewrite and simplify, it could be implemented by using current tactics, possibly...
@gabrielhdt What is the effect of having an .ocamlformat file?
In the current syntax: ``` symbol Set: TYPE; injective symbol η: Set → TYPE; symbol arr: Set → Set → Set; rule η (arr $X $Y) ↪ (η $X) →...
Requires https://github.com/Deducteam/lambdapi/issues/1010 to be fixed first.
The RHS extra variables lack information about their sort, which makes unification fails. In Eval.tree_walk, case Leaf, a `TEnv` is replaced by a `Plac false`, that is, not a type....
To know which pairs ocaml-camlp5 work, see https://github.com/jrh13/hol-light/pull/71.
Hi. Currently no. But there are various ongoing works to do this. From Coq, you can go to Dedukti using https://github.com/Deducteam/coqine/, and from Isabelle, you can go to Dedukti and...
Hi Thiago. Here are a few first questions/remarks: - Why "if R is locally confluent without using beta to close critical pairs and moreover R is SN then R+beta is...