Frédéric Blanqui
Frédéric Blanqui
What is Prop?
Do you mean things like inductive predicates? ``` Prop:TYPE Prf:Prop -> TYPE inductive N:TYPE := O:N | s:N -> N le:N -> N -> Prop le_refl x: Prf(le x x)...
It just needs to be implemented. The current inductive command needs to be extended for looking at terms of the form (Prf (le _ _)) instead of (le _ _)...
Could you please provide an example?
Strictly speaking, expressions like $x are not metavariables; they are pattern variables. They have user-defined names. Metavariables have no user-defined names. Metavariables are generated by the system. Some long time...
Not immediately but feel free to make a PR ;-) It shouldn't be too difficult. At the end of sr.ml, in the constraints, you need to replace function symbols $i...
In the second case, no unification problems are generated. Moreover a metavariable depends on all the bound variables occurring before. So we probably have a quadratic complexity here.
Hi @Rehan-MALAK . Thank you for your issue. Could you please give more details about the problems you get because of this line, and with which versions of emacs and...
Hi. I don't know if it makes a difference but why don't you install the emacs mode from melpa? make install_emacs_mode should be used for local testing only. My own...
Thank you for your PR @Rehan-MALAK !