Stream: Coq users

Topic: Weird error with induction


view this post on Zulip Ali Caglayan (Apr 21 2021 at 13:56):

I'm getting a weird error with the induction tactic: Cannot remove n. [cannot-remove-as-expected,tactics] as far as I can tell, Jason has been able to reproduce the error on github and opened a bug report, but nobody has looked at it: https://github.com/coq/coq/issues/10766

view this post on Zulip Ali Caglayan (Apr 21 2021 at 13:56):

Anybody understand what is going on?


Last updated: Jan 29 2023 at 05:03 UTC