Commit 2020-04-10 18:03 61fa4896
View on Github →feat(tactic/trunc_cases): a tactic for case analysis on trunc hypotheses (#2368)
/--
Perform case analysis on a `trunc` expression,
preferentially using the recursor `trunc.rec_on_subsingleton`
when the goal is a subsingleton,
and using `trunc.rec` otherwise.
Additionally, if the new hypothesis is a type class,
reset the instance cache.
-/