5 votes

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

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