fix(tactic/lint): simp_nf: do not ignore errors #2266
mergify
merged
25 commits into
master
from
simp-nf2-lint
lint for lemmas whose lhs does not simplify
e1572e3c
Be stricter about checking equality of terms.
af57bf1a
Support general equivalence relations.
ceafb44f
Revert "Support general equivalence relations."
bef5cab4
Ignore definitions with equation lemmas.
251802f0
Centralize error checking in linters.
2b58e49c
Clean up a bit.
b278cc76
Fix loop with ⇑↑f = ⇑f
f5c6dd85
Fix simp lemmas that don't work
a9c8b17e
Remove simp attribute.
2f4b7d90
Correctly define coercions to functions for continuous_linear_map
dd8b760e
Correctly define function coercion for linear equivalences.
3b69afd5
Remove simp lemma that doesn't work
1dd86a4e
Remove simp from unitality axioms.
2c2dfe50
Fix ordinal proof.
a8df4a09
Replace subsingleton.{is_open,is_closed} by discrete topology instance
82cf1d6e
Fix proofs in times_cont_diff
db072623
Add library note for function coercions.
15145fe3
Merge remote-tracking branch 'origin/master' into simp-nf2-lint
9f9b1ce1
Reference library note.
64faadb3
Retract advice on building has_coe_to_fun instances using coercions.
77cc6185
robertylewis
approved these changes
on 2020-03-30
Change back proofs in times_cont_diff.
4505c9bf
Merge remote-tracking branch 'origin/master' into simp-nf2-lint
24a41e56
Fix build.
f27c598a
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into simp-nf2-lint
3c57097d
Login to write a write a comment.
Login via GitHub