Zulip Chat Archive

Stream: Is there code for X?

Topic: le on option


view this post on Zulip 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:.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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