mathlib3
26bdcac0 - chore(coinductive_predicates): remove private and use of import_private (#10084)

Commit
4 years ago
chore(coinductive_predicates): remove private and use of import_private (#10084) Remove a `private` modifier (I think this had previously been ported from core by @bryangingechen). Then remove the only use of `import_private` from the library. (Besides another use in `tests/`, which we're not porting.) (In mathlib4 we have `OpenPrivate` as an alternative. Removing `import_private` is one less thing for mathport to care about.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading