Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-09 11:59 fb63cf3e

View on Github →

chore(data/pfun): rename roption to part, split data.part off data.pfun (#8544)

Estimated changes

modified theorem computable.of_option
deleted theorem computable.part
deleted theorem computable₂.part
modified theorem decidable.partrec.const'
modified def nat.rfind
modified def nat.rfind_opt
modified theorem partrec.const'
modified theorem partrec.none
modified theorem nat.partrec.code.eval_const
modified theorem nat.partrec.code.eval_id
modified def turing.TM0.eval
modified def turing.TM1.eval
modified def turing.TM2.eval
modified def turing.eval
added def part.fix.approx
added def part.fix_aux
added theorem part.fix_def'
deleted def roption.fix.approx
deleted def roption.fix_aux
deleted theorem roption.fix_def'
added theorem part.fix.approx_le_fix
added theorem part.fix.approx_mono'
added theorem part.fix.approx_mono
added theorem part.fix.mem_iff
added theorem part.fix_eq
added theorem part.fix_eq_ωSup
added theorem part.fix_le
added theorem part.to_unit_cont
deleted theorem roption.fix.approx_le_fix
deleted theorem roption.fix.approx_mono'
deleted theorem roption.fix.approx_mono
deleted theorem roption.fix.mem_iff
deleted theorem roption.fix_eq
deleted theorem roption.fix_eq_ωSup
deleted theorem roption.fix_le
deleted theorem roption.to_unit_cont
modified theorem enat.coe_inj
modified theorem enat.ne_top_iff
modified def enat
added def part.assert
added theorem part.assert_defined
added theorem part.assert_neg
added theorem part.assert_pos
added theorem part.bind_assoc
added theorem part.bind_defined
added theorem part.bind_dom
added theorem part.bind_eq_bind
added theorem part.bind_le
added theorem part.bind_map
added theorem part.bind_none
added theorem part.bind_some
added theorem part.bind_some_eq_map
added theorem part.bind_some_right
added theorem part.coe_none
added theorem part.coe_some
added theorem part.dom_iff_mem
added theorem part.eq_none_iff'
added theorem part.eq_none_iff
added theorem part.eq_some_iff
added theorem part.eta
added theorem part.ext'
added theorem part.ext
added theorem part.get_eq_get_of_eq
added theorem part.get_eq_of_mem
added theorem part.get_mem
added def part.get_or_else
added theorem part.get_or_else_none
added theorem part.get_or_else_some
added theorem part.get_some
added def part.map
added theorem part.map_bind
added theorem part.map_eq_map
added theorem part.map_id'
added theorem part.map_map
added theorem part.map_none
added theorem part.map_some
added theorem part.mem.left_unique
added theorem part.mem_assert
added theorem part.mem_assert_iff
added theorem part.mem_bind
added theorem part.mem_bind_iff
added theorem part.mem_coe
added theorem part.mem_eq
added theorem part.mem_map
added theorem part.mem_map_iff
added theorem part.mem_of_option
added theorem part.mem_restrict
added theorem part.mem_some
added theorem part.mem_some_iff
added theorem part.mem_to_option
added theorem part.mem_unique
added theorem part.ne_none_iff
added def part.none
added theorem part.not_mem_none
added def part.of_option
added theorem part.of_option_dom
added theorem part.of_option_eq_get
added theorem part.of_to_option
added theorem part.pure_eq_some
added def part.restrict
added theorem part.ret_eq_some
added def part.some
added theorem part.some_get
added theorem part.some_inj
added theorem part.some_ne_none
added theorem part.to_of_option
added def part.to_option
added structure {u}
modified def pfun
deleted def roption.assert
deleted theorem roption.assert_defined
deleted theorem roption.assert_neg
deleted theorem roption.assert_pos
deleted theorem roption.bind_assoc
deleted theorem roption.bind_defined
deleted theorem roption.bind_dom
deleted theorem roption.bind_eq_bind
deleted theorem roption.bind_le
deleted theorem roption.bind_map
deleted theorem roption.bind_none
deleted theorem roption.bind_some
deleted theorem roption.bind_some_eq_map
deleted theorem roption.bind_some_right
deleted theorem roption.coe_none
deleted theorem roption.coe_some
deleted theorem roption.dom_iff_mem
deleted theorem roption.eq_none_iff'
deleted theorem roption.eq_none_iff
deleted theorem roption.eq_some_iff
deleted theorem roption.eta
deleted theorem roption.ext'
deleted theorem roption.ext
deleted theorem roption.get_eq_get_of_eq
deleted theorem roption.get_eq_of_mem
deleted theorem roption.get_mem
deleted def roption.get_or_else
deleted theorem roption.get_or_else_none
deleted theorem roption.get_or_else_some
deleted theorem roption.get_some
deleted def roption.map
deleted theorem roption.map_bind
deleted theorem roption.map_eq_map
deleted theorem roption.map_id'
deleted theorem roption.map_map
deleted theorem roption.map_none
deleted theorem roption.map_some
deleted theorem roption.mem.left_unique
deleted theorem roption.mem_assert
deleted theorem roption.mem_assert_iff
deleted theorem roption.mem_bind
deleted theorem roption.mem_bind_iff
deleted theorem roption.mem_coe
deleted theorem roption.mem_eq
deleted theorem roption.mem_map
deleted theorem roption.mem_map_iff
deleted theorem roption.mem_of_option
deleted theorem roption.mem_restrict
deleted theorem roption.mem_some
deleted theorem roption.mem_some_iff
deleted theorem roption.mem_to_option
deleted theorem roption.mem_unique
deleted theorem roption.ne_none_iff
deleted def roption.none
deleted theorem roption.not_mem_none
deleted def roption.of_option
deleted theorem roption.of_option_dom
deleted theorem roption.of_option_eq_get
deleted theorem roption.of_to_option
deleted theorem roption.pure_eq_some
deleted def roption.restrict
deleted theorem roption.ret_eq_some
deleted def roption.some
deleted theorem roption.some_get
deleted theorem roption.some_inj
deleted theorem roption.some_ne_none
deleted theorem roption.to_of_option
deleted def roption.to_option
deleted structure {u}
added theorem part.eq_of_chain
added theorem part.mem_ωSup
added theorem part.ωSup_eq_none
added theorem part.ωSup_eq_some
modified def preorder_hom.bind
deleted theorem roption.eq_of_chain
deleted theorem roption.mem_ωSup
deleted theorem roption.ωSup_eq_none
deleted theorem roption.ωSup_eq_some
added theorem part.examples.div.cont
added theorem part.examples.f91.cont
added theorem part.examples.f91_dom
added theorem part.examples.f91_spec
added inductive part.examples.tree
deleted theorem roption.examples.div.cont
deleted theorem roption.examples.f91.cont
deleted theorem roption.examples.f91_dom
deleted theorem roption.examples.f91_spec
deleted inductive roption.examples.tree