feat(tactic/ring_exp) allow ring_exp inside of conv blocks #2369
mergify
merged
6 commits into
master
from
ring_exp-conv
allow ring_exp inside of conv blocks
a597328e
alexjbest
changed the title 
kim-em
commented
on 2020-04-09
Update test/ring_exp.lean
395708ed
kim-em
commented
on 2020-04-09
Update test/ring_exp.lean
2185bd03
kim-em
commented
on 2020-04-09
Update test/ring_exp.lean
5ae52b18
kim-em
commented
on 2020-04-09
add docstrings
ecaa56bb
kim-em
approved these changes
on 2020-04-09
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into ring_exp-conv
f110a2de
Login to write a write a comment.
Login via GitHub