## Stream: Is there code for X?

### Topic: le on option

#### Marcus Rossel (Mar 09 2021 at 16:56):

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 (Mar 09 2021 at 17:04):

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 (Mar 09 2021 at 17:08):

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 (Mar 09 2021 at 17:37):

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

#### Marcus Rossel (Mar 09 2021 at 19:30):

Eric Wieser said:

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

Almost missed that, thanks :)

Last updated: May 17 2021 at 15:13 UTC