Stream: Coq users

Topic: Naming induction hypothesis


view this post on Zulip 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?

view this post on Zulip Théo Winterhalter (Jan 17 2022 at 21:22):

Do you mean that induction ... as doesn't work?

view this post on Zulip 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: Jan 27 2023 at 01:03 UTC