mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Probably `setup_tactic_parser` can be integrated to use `open_locale` instead

Open khoek opened this issue 6 years ago • 4 comments

khoek avatar Sep 20 '19 14:09 khoek