mathlib
d40662f5 - chore(tactic/auto_cases): add docstring and remove duplication (#2488)

Commit

5 years ago

chore(tactic/auto_cases): add docstring and remove duplication (#2488) I was just adding a docstring, and I saw some duplication so I removed it too. <br> <br> <br>

References

#2700 - Fix merge conflict

Author

khoek

Parents

f760ad5f

mathlib d40662f5 - chore(tactic/auto_cases): add docstring and remove duplication (#2488)

mathlib
d40662f5 - chore(tactic/auto_cases): add docstring and remove duplication (#2488)