3 ms·
> I don't understand what this is supposed to mean. How are e.g. coq tactics not the exact same? Well, I've never gotten `induction' to generate anything close
by remexre 6y ago
> I don't understand what this is supposed to mean. How are e.g. coq tactics not the exact same?
Well, I've never gotten `induction' to generate anything close to a readable program -- hopefully this is better?
- ImprobableTruth 6y agoI'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 agoIIRC, 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.