Kim Morrison
|
c3948cba24
|
feat: upstream definition of Vector from Batteries (#6197)
This PR upstreams the definition of `Vector` from Batteries, along with
the basic functions.
|
2024-11-24 23:01:32 +00:00 |
|
Leonardo de Moura
|
e53435979f
|
fix: remove hacky addAutoBoundImplicitsOld
|
2022-03-25 09:23:43 -07:00 |
|
Leonardo de Moura
|
6631d92d7b
|
fix: addAutoBoundImplicitsOld occurrences at MutualDef.lean and Structure.lean
This commit also fixes non-termination at `collectUnassignedMVars`
|
2022-03-25 09:07:59 -07:00 |
|
Leonardo de Moura
|
e48cc8901e
|
fix: add new addAutoBoundImplicits that avoids the hack at addAutoBoundImplicitsOld
|
2022-03-25 08:40:57 -07:00 |
|