Nicolas Tabareau
Nicolas Tabareau
> It never becomes a neutral term, as it unfolds to a `fix` construct. > Indeed, I think you are right, mentioning potential extension of definitions as symbols was a...
Thx @gasche for your feedback. All that you say here is fairly right, what I am missing is the motivation. If you can inhabit an axiom within Coq, then it...
Ok, so maybe the problem is rather the lack of abstraction/parametrization of our current version of rewrite rules. As you noticed in our paper, we have a paragraph "Abstracting over...
> By the way, why make it an a posteriori check? Indeed, we can force rewrite rules to already holds propositionally, and this is how it is implemented in Agda....
@herbelin do you think it is doable ?
@coqbot run full ci
@coqbot run full ci
@coqbot bench
@jdchristensen the gain on coq-hott is not huge, but significant enough > coq-hott │ 155.24 157.85 -1.65 │ 1063561633649 1086483238308 -2.11 │