Stream: math-comp users

Topic: ✔ Are inductive propositions unidiomatic in ssreflect?

Notification Bot (Sep 02 2022 at 00:35):

abab9579 has marked this topic as resolved.

abab9579 (Sep 02 2022 at 00:59):

By the way, it turned out me NOT simplifying was causing problem. That caused it to (likely) go for normal form when it had to be reduced.

Last updated: Feb 08 2023 at 07:02 UTC