Mark Raynsford (Jan 17 2022 at 21:01): Mark Raynsford (Jan 17 2022 at 21:01):Hello! I'm running with Mangle Names in order to ensure that my proofs aren't dependent on generated names. For some reason, I'm stuck trying to supply a name for a generated induction hypothesis. There doesn't seem to be a way to tell the induction tactic what name to use... Is this expected right now?
Théo Winterhalter (Jan 17 2022 at 21:22):Do you mean that induction ... as doesn't work?
Mark Raynsford (Jan 17 2022 at 22:11):Sorry, I've just realized I made a mistake. I was missing the last parameter to as, so the induction hypothesis was using a generated name.
Last updated: Oct 13 2024 at 01:02 UTC