Commit 2022-11-07 03:58 fd97e04c

View on Github →

feat: port Data.Option.Basic (#493)

  • Define getOrElse here -- likely belongs in Std
  • lemmas mentioning coe now use up-arrow, even though that refers to some directly
  • Option.elim has different argument order

Estimated changes

added theorem Option.Mem.left_unique
added theorem Option.bind_eq_bind
added theorem Option.bind_eq_none'
added theorem Option.bind_eq_some'
added theorem Option.bind_pmap
added def Option.casesOn'
added theorem Option.casesOn'_coe
added theorem Option.casesOn'_none
added theorem Option.casesOn'_some
added theorem Option.choice_eq_none
added theorem Option.coe_def
added theorem Option.coe_get
added theorem Option.elim_none_some
added theorem Option.getD_coe
added theorem Option.guard_eq_some'
added theorem Option.iget_mem
added theorem Option.iget_of_mem
added theorem Option.joinM_eq_join
added theorem Option.map_bind'
added theorem Option.map_bind
added theorem Option.map_coe'
added theorem Option.map_coe
added theorem Option.map_comm
added theorem Option.map_comp_some
added theorem Option.map_eq_id
added theorem Option.map_inj
added theorem Option.map_injective'
added theorem Option.map_pbind
added theorem Option.map_pmap
added theorem Option.mem_pmem
added theorem Option.none_bind'
added theorem Option.none_orElse'
added theorem Option.orElse_eq_none'
added theorem Option.orElse_eq_none
added theorem Option.orElse_eq_some'
added theorem Option.orElse_eq_some
added theorem Option.orElse_none'
added theorem Option.pbind_eq_bind
added theorem Option.pbind_eq_none
added theorem Option.pbind_eq_some
added theorem Option.pbind_map
added theorem Option.pmap_bind
added theorem Option.pmap_eq_map
added theorem Option.pmap_map
added theorem Option.pmap_none
added theorem Option.pmap_some
added theorem Option.seq_some
added theorem Option.some_bind'
modified theorem Option.some_injective
added theorem Option.some_orElse'