mathlib3
94dcadd5 - feat(test/polyrith): better formatting for generated tests (#15728)

Commit
3 years ago
feat(test/polyrith): better formatting for generated tests (#15728) The `polyrith` test suite is unusually structured to avoid making dozens of calls to Sage. A helper tactic calls `polyrith` and saves the output from Sage along with intermediate information, printing a full test as a "Try this:". This PR makes that helper tactic format its output better, spread over multiple lines as requested at https://github.com/leanprover-community/mathlib/pull/15292#discussion_r925838661 by @eric-wieser . Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Author
Parents
Loading