le on option

Stream: Is there code for X?

[Marcus Rossel]

Is there an easy way to get ≤ for option ℕ?
I understand that there are multiple ways one could define it, but perhaps there's a "standard" way. Currently I just have:

def optional_le : option ℕ → option ℕ → Prop
| _        none      := false
| none     _         := true
| (some p) (some p') := p ≤ p'

The reason I ask is that I'm trying to avoid showing:

instance : is_total (option ℕ) optional_le := sorry
instance : is_antisymm (option ℕ) optional_le := sorry
instance : is_trans (option ℕ) optional_le := sorry
instance : decidable_rel optional_le := sorry

Also, I've just noticed that this relation isn't total :grimacing:.

[Floris van Doorn]

There is a definition docs#with_bot which is the same as option, but comes with a specified order, and the new element \bot is the least element. Compare docs#with_top.

[Floris van Doorn]

This works out of the box:

import order.bounded_lattice

example : linear_order (with_bot ℕ) :=
by apply_instance

example : decidable_rel ((≤) : with_bot ℕ → with_bot ℕ → Prop) :=
by apply_instance

[Eric Wieser]

I assume you meant to define | none none := true, which is what the types Floris references do

[Marcus Rossel]

Eric Wieser said:

I assume you meant to define | none none := true, which is what the types Floris references do

Almost missed that, thanks :)