match on option

Stream: general

[Scott Morrison]

if I have o : option A, and write

match o with
| some a := ...
| none := ...
end

how can I access the fact o.is_none in the second branch?

[Scott Morrison]

Of course I could write an if h : o.is_some then ... else ..., at the cost of slightly less pretty extraction of the some.

[Mario Carneiro]

you could match on o, o.is_some, rfl : \forall o b, o.is_some = b -> ... with some a, tt, rfl and none, ff, rfl

[Bryan Gin-ge Chen]

(deleted)

[Kevin Buzzard]

This match on rfl technique comes up once every couple of months. Examples of this technique should be put in the docs