Commit 2024-07-24 13:07 bbbb785d
View on Github →chore: address elab_as_elim
workarounds (#15091)
There were a number of places that eliminator elaboration was suppressed using the (motive := _)
trick to be used in conjuction with apply
, but it's generally clearer to use induction
, refine
, or, sometimes, rintro
(for Quot
).