3 ms·

I'm not sure what you mean? The induction tactic uses the induction principle (dependent eliminator) of the corresponding type. If you unfold the dependent elim

I'm not sure what you mean? The induction tactic uses the induction principle (dependent eliminator) of the corresponding type. If you unfold the dependent eliminator, it boils down to a combination of fix and match. I don't see how you could get a term simpler than that, unless you mean something else by readable?

remexre 6y ago
IIRC, the match it generates often ends up being a dependent match using the convoy pattern once nontrivial functions start being written, which quickly gets really really hard to read. Maybe this is partly the fault of Coq's matching requiring the convoy pattern (unlike Agda's or Idris's), but I find it extremely difficult to read these terms, versus hand-written ones.