Commit 2020-01-26 19:37 587b312e
View on Github →refactor(order/filter/basic): redefine filter.pure
(#1889)
- refactor(order/filter/basic): redefine
filter.pure
New definition hass ∈ pure a
definitionally equal toa ∈ s
. - Update src/order/filter/basic.lean Co-Authored-By: Gabriel Ebner gebner@gebner.org
- Minor fixes suggested by @gebner
- Fix compile
- Update src/order/filter/basic.lean