Zulip Chat Archive

Stream: mathlib4

Topic: List.Mem as Or?


Arien Malec (Jan 11 2023 at 20:17):

In data.prod.tprod we have hj : j ∈ i :: l and then hj.resolve_left which seems like hj is being coerced to an or but I haven't been able to see where that coercion is happening in mathlib. Post mathport, this doesn't work at all. What's going on on in mathlib and what's the mathlib 4 equivalent?

Chris Hughes (Jan 11 2023 at 20:23):

The definition of j in i :: l in Lean3 is j=i or j in l. In lean4 the definition changed so you have to write (mem_cons.2 hj).resolve_left

Arien Malec (Jan 11 2023 at 20:30):

mem_cons.mp rather than mem_cons.mpr at it happens.


Last updated: Dec 20 2023 at 11:08 UTC