Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-02 04:37 69094fcf

View on Github →

fix(tactic/library_search): iff lemmas with universes (#935)

fix(tactic/library_search): iff lemmas with universes
cleaning up
add crossreference

Estimated changes

Modified src/tactic/basic.lean

Modified src/tactic/library_search.lean

Modified test/library_search/basic.lean

added def test.library_search.P

added def test.library_search.Q

added def test.library_search.f

Created test/library_search/ordered_ring.lean