mathlib
b1654df1
- feat(meta/rb_map,tactic/monotonicity): replace rb_map.insert_cons (#1571)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
feat(meta/rb_map,tactic/monotonicity): replace rb_map.insert_cons (#1571) rb_map key (list value) is the same as rb_lmap. Usages of this function should be replaced with rb_lmap.insert
References
#1571 - chore(meta/rb_map,tactic/monotonicity): replace rb_map.insert_cons
Author
robertylewis
Committer
mergify[bot]
Parents
74bed0c9
Loading