5 votes
Accepted

Is unguarded fixpoint reduction consistent?

This is consistent. First, this equality holds propositionally by eta-expansion of the constructor. Thus, if your type theory had equality reflection, it would also hold definitionally. Since ...
Pierre-Marie Pédrot's user avatar
3 votes
Accepted

Coq simpl failing to do beta reduction in this fixpoint expression

There is no reduction to be done, which is why simpl isn't doing anything. First of all, concat_aux is not a double fixpoint, ...
Ana Borges's user avatar
2 votes

Defining a Recursive Function decreasing on one argument with < and another structurally

I rephrased the * case into : ...
Pierre Castéran's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible