Def makeSingleton

Modification history

2025-09-01 17:39
MathlibTest/RewriteSearch/Basic.lean
chore: remove `rw_search` tactic (#29196) …
Deleted makeSingletonView on Github →
2023-11-02 03:46
test/RewriteSearch/Basic.lean
fix: add withMainContext to rw_search, and add a test case (#8101) …
Added makeSingletonView on Github →