diff options
| author | Cyril Cohen | 2020-09-08 03:25:04 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-28 16:03:52 +0200 |
| commit | fab8ceb34957ca4e261a5ba91cf8379f694dd1b8 (patch) | |
| tree | 570b5622a69d92d21098248cfbf051e71672bbd7 /mathcomp/ssreflect | |
| parent | 85166cd6c9074f96e71ebce91e2d1243fabada64 (diff) | |
Update `map_mx_id`, fix some implicits and argument orders
- Fix implicits of `eq_map_mx`, `eq_in_map_mx`, `map_mx_id_in` and `map_mx_id`,
in order to give more practical arguments first.
- Generalized `map_mx_id` to take the shape f =1 id -> M ^ f = M.
The previous behaviour can be recovered through `map_mx_id (frefl id)` or `[_ ^ id]map_mx_id`
Diffstat (limited to 'mathcomp/ssreflect')
0 files changed, 0 insertions, 0 deletions