Array.map def_eq

Stream: lean4

[Violeta Hernández]

How come the first is def-eq but the second isn't?

-- works
example : ([1, 1, 1].map (· + 1))[1] = 2 := rfl
-- fails
example : (#[1, 1, 1].map (· + 1))[1] = 2 := rfl

[Violeta Hernández]

(on a somewhat related note, we seem to be missing Array.getElem_map for Batteries.Vector)

[Violeta Hernández]

Oh I see, docs#Array.mapM.map is irreducible

[Violeta Hernández]

What's the reasoning behind this?

[Mario Carneiro]

it's because it's defined by well founded recursion, these get automatically marked as irreducible

[Violeta Hernández]

This can be overriden, right? Would it make sense to PR that change?

[Kim Morrison]

Works fine on nightly-testing. (In general at the moment, anything to do with Array should be assumed to possibly work differently on nightlies. :-)

[Kim Morrison]

getElem_map for Batteries.Vector would be nice, though!