mathlib
fde1fc28 - feat(*): make more non-instances reducible (#8941)

Commit

4 years ago

feat(*): make more non-instances reducible (#8941) * Also add some docstrings to `cau_seq_completion`. * Related PR: #7835

Author

fpvandoorn

Parents