mathlib3
d85af62f - chore(tactic/fix_reflect_string): delete file (#15537)

Commit
3 years ago
chore(tactic/fix_reflect_string): delete file (#15537) The file `tactic/fix_reflect_string` has a header from @gebner explaining that it was written as a workaround for the Lean issue [144](https://github.com/leanprover-community/lean/issues/144): ```quote The default `has_reflect string` instance in Lean only work for strings up to few thousand characters. Anything larger than that will trigger a stack overflow because the string is represented as a very deeply nested expression ``` This issue was fixed in [185](https://github.com/leanprover-community/lean/pull/185) and at least one file which imports it, `tactic/doc_commands`, no longer uses its contents. Can we delete the file forever now? Or should we keep it because the workaround might be useful in the future? Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Author
Parents
Loading