mathlib3
996ece59 - feat(tactic/suggest): add a flag to disable "Try this" lines (#9820)

Commit

4 years ago

feat(tactic/suggest): add a flag to disable "Try this" lines (#9820)

Author

jcommelin

jcommelin

Parents

Loading