feat(tactic/equiv_rw): incorporating equiv_functor #2301
mergify
merged
151 commits into
master
from
equiv_rw_functorial
feat(tactic): rewriting along equivalences
b29e41b8
header
a202cc24
minor
cbca24ae
type
98fb8104
actually, rewriting the goal under functors is easy
12c646eb
rewriting inside function types
2fbf8e23
more
68c68ca9
way better
cd4e7bb5
improving comments
d65a8a23
fun
3a0dcac3
feat(data/equiv): pi_congr
0ce88626
various
ca2f911b
feat(data/equiv): sigma_congr
c104ab0f
docstrings
beeb1f52
change case for consistency
732b0ec3
tidying up
120219bd
Merge branch 'sigma_congr' into equiv_rw
b2771b44
merge
5de7c5a4
minor
064b74de
minor
47ba35d3
switching names
3d86aa49
fixes
1577c622
Merge branch 'equiv.pi_congr' into equiv_rw
e07ba898
Merge remote-tracking branch 'origin/master' into equiv_rw
564ff5a2
add some tracing routines for convenience
6e9062ff
feat(tactic/core): trace_for
df77662e
typo
142b9d29
oops
a6d61174
oops
87ec7c90
Merge remote-tracking branch 'origin/master' into trace_for
1b62bcdc
merge
6c749b1b
various
cd37aa11
chore(tactic/solve_by_elim): cleanup
4033570a
cleanup
b680dafd
what happened to my commit?
f86fb333
fix
a81942f6
fix
87fcc485
rename to trace_if_enabled
1ba32577
fixed?
8521631c
Tweak comments
aa1781e5
feat(tactic/solve_by_elim): add accept parameter to prune tree search
1b7877cc
when called with empty lemmas, use the same default set as the intera…
b9c0f351
Merge branch 'solve_by_elim_cleanup' into solve_by_elim_accept
53bb8513
trace_state_if_enabled
ca085f30
Update src/data/equiv/basic.lean
5e863797
implicit arguments
999fd41f
Merge remote-tracking branch 'origin/master' into equiv.pi_congr
28fa982f
stop cheating with [] ~ none
13fa4bc5
Merge remote-tracking branch 'origin/master' into solve_by_elim_cleanup
e31120dc
merge
a838470c
indenting
2afd7d34
Merge branch 'solve_by_elim_accept' into equiv_rw
98ec6513
Merge remote-tracking branch 'origin/trace_for' into equiv_rw
0b650b18
yay, working via solve_by_elim
e637cd89
pretty good
b682ab3b
various
259ad741
various
d1db7958
Merge branch 'solve_by_elim_accept' into equiv_rw
af58d055
docstring
d5a8bad9
merge
adc16a6b
fix docstrings
c3ba895d
Merge branch 'solve_by_elim_cleanup' into solve_by_elim_accept
c23d5baf
more docs
258db37f
docs
04ddcf12
Merge branch 'solve_by_elim_accept' into equiv_rw
c8cc21de
feat(data/equiv/functor): bifunctor.map_equiv
af830fde
Merge branch 'bifunctor.map_equiv' into equiv_rw
43e2874a
bifunctors
b4bfdf11
test rewriting under unique
19c100ff
start
bf3e99d5
Merge branch 'bifunctor.map_equiv' into equiv_functor
5638f813
sketch of equiv_functor
28c216f2
rewriting in subtypes
e9f124c7
add documentation, and make the function an explicit argument
42594503
documentation
92ed6134
fix doc-strings
46bea2db
Merge branch 'solve_by_elim_accept' into equiv_rw
b02734a3
typos
0776ffda
minor
6bc98345
adding demonstration of transporting semigroup
0695b447
update
248bf481
removing unimpressive inhabited example; easier later
56618162
merge
7f109500
Update .vscode/settings.json
7564ae5d
Merge branch 'equiv.pi_congr' into equiv_rw
cf77734a
Merge branch 'equiv_rw' of github.com:leanprover-community/mathlib in…
c877bcbb
err
0929b3e3
trying to transport through monoid
12d50cf1
err?
4c4da66a
merge
552ef978
Merge branch 'solve_by_elim_accept' into equiv_rw
0cf48aeb
Merge branch 'bifunctor.map_equiv' into equiv_rw
1a8ec5f6
much better
9f227a7e
improve documentation of accept, and add doc-string
5356daaf
Merge remote-tracking branch 'origin/master' into solve_by_elim_accept
b66cc7fd
merge
f0f4db62
fix duplicated namespace
ac840139
improve docs
e1c7ce9b
Merge branch 'solve_by_elim_accept' into equiv_rw
7bcd77c8
merge
2b7a0c35
feat(logic/basic): trivial transport lemmas
1a1ad0ef
try again with documentation
e9b6cc3e
Merge branch 'solve_by_elim_accept' into equiv_rw
719b64b6
update
d35b2fc0
oops
98e7cfe4
oops
7f86ae9f
omit
ecb03ce8
revert unnecessary change
452c3e9b
fix doc-string
30c3a96d
Merge branch 'equiv_functor' of github.com:leanprover-community/mathl…
9c52fefc
Merge branch 'equiv_functor' into equiv_rw_functorial
d651ff2a
Merge branch 'trivial-transport' into equiv_rw_functorial
4ebf66eb
chore(data/equiv/basic): simp to_fun to coe
27140fd8
Merge branch 'to_fun_as_coe' into equiv_rw_functorial
8c41f000
feat(tactic/equiv_rw): incorporating equiv_functor
624965fa
rename adapt_equiv
741cdec1
simplify the equivalence produced, and provide a tactic to access the…
0a0e6fa0
add max_steps option
0fcd8d58
add decl_name to add_tactic_doc
44706231
fix add_tactic_doc
0dd3d529
satisfying linter
6172a7ab
merge
6b9553ac
fix names
84e42a35
finish fix
14e19889
Merge branch 'equiv_functor' into equiv_rw_functorial
0f917ef5
add defaults for cfg arguments
03b7f1e0
merge
30259389
merge
3fff53e5
remove simplify_term, which already existed as expr.simp
04d14df8
remove duplicate functions that have been PRd separately
8f9cc7fc
Merge remote-tracking branch 'origin/master' into equiv_rw
c59d4624
no need for accept
932e079e
Update src/tactic/equiv_rw.lean
127deef1
Update src/tactic/equiv_rw.lean
0b8dfaef
replace max_steps with max_depth
639f93e4
use solve_aux
9620e5e9
Merge branch 'equiv_rw' of github.com:leanprover-community/mathlib in…
bf9e2999
add missing simp lemmas about arrow_congr'
eb03d09e
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into equiv_rw
2ee768b1
Merge branch 'master' into equiv_rw
4f80b5a1
Merge branch 'master' into equiv_rw
7d2424ca
fix failing test, by making sure we don't leave any ≃ goals on the table
648eaaa4
add comment
01dc6c23
Merge branch 'equiv_rw' into equiv_rw_functorial
1edd1ebe
comment out trace output
1cc3aa01
fix fields
24f028e1
Merge branch 'equiv_rw' into equiv_rw_functorial
e7c9981a
Merge remote-tracking branch 'origin/master' into equiv_rw_functorial
9543dbce
Merge branch 'master' into equiv_rw
43c5284f
Merge branch 'equiv_rw' into equiv_rw_functorial
07bf8d51
merge
2dc08ec8
gebner
approved these changes
on 2020-03-31
Login to write a write a comment.
Login via GitHub