mathlib3
feat(tactic): new tactics to normalize casts inside expressions
#988
Merged
Merged
feat(tactic): new tactics to normalize casts inside expressions #988
mergify
merged
32 commits into
leanprover-community:master
from
pnmadelaine:norm_cast
new tactics for normalizing casts
f61b36ad
update using the norm_cast tactics
6dea9d24
minor proof update
15aadb7a
minor changes
2120d65f
moved a norm_cast lemma
bd3041bf
minor changes
ec120d8c
fix(doc/tactics): make headers uniform
e6e07c2d
nicer proof using discharger
856eaabb
fixed numerals handling by adding simp_cast lemmas
7951a622
add documentation
6bc6e6e4
fixed unnecessary normalizations in assumption_mod_cast
42459395
minor proof update
76be0e9b
minor coding style update
cd4ff43e
documentation update
f8112802
Merge branch 'master' into norm_cast
c06e1c68
rename flip_equation to expr.flip_eq
5e19305a
update proofs to remove boiler plate code about casts
6f920080
Merge branch 'master' into norm_cast
9ece6bba
pnmadelaine
commented
on 2019-05-07
revert to old proof
8280a8fe
fixed imports and moved attributes
5f99060b
add test file
ccbb5364
new attribute system
f4bf43fa
syntax fix
752b6b84
change attributes names
0cef9461
Merge branch 'master' into norm_cast
6b4b0865
test update
2873635f
small update
f37aec25
Merge branch 'master' into norm_cast
52a36fcd
add elim_cast attribute
511bab17
add examples for attributes
c1509410
new examples
da98a79e
Merge branch 'master' into norm_cast
5ce98229
digama0
approved these changes
on 2019-05-14
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub