search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
198 stars 35 forks source link

Modify `ring` tactic #61

Closed joneugster closed 1 year ago

joneugster commented 1 year ago

Modify ring tactic so you can use it non-terminal without info about ring_nf being shown.

Also modify the level(s) introducing ring accordingly.

joneugster commented 1 year ago

moved.