Option.get

Stream: mathlib4

[Kevin Buzzard]

In Lean 4 (well, in Std) o is explicit: def Option.get {α : Type u} : (o : Option α) → isSome o → α and in Lean 3 it's implicit. Presumably this is beyond the capabilities of the autoporter?

[Mario Carneiro]

yes

[Mario Carneiro]

backporting is also an option, I think the lean 4 definition is better

[Kevin Buzzard]

yeah I'm live streaming porting on the Discord and Chris Hughes just agreed with you.

[Yaël Dillies]

Yeah, I had plans to make it explicit because I always got into the dumbest type ascriptions using it.