Mathlib Changelog
Changelog
About
Github
Commit
2018-05-19 21:28
fc20442e
View on Github →
feat(computability/partrec): partial recursion, Godel numbering
Estimated changes
Modified
data/bool.lean
added
theorem
bool.ff_eq_to_bool_iff
added
theorem
bool.tt_eq_to_bool_iff
Modified
data/computability/partrec.lean
added
theorem
computable.comp
added
theorem
computable.comp₂
added
theorem
computable.const
added
theorem
computable.fst
added
theorem
computable.nat_elim
added
theorem
computable.of_eq
added
theorem
computable.of_option
added
theorem
computable.pair
added
theorem
computable.part
added
theorem
computable.snd
added
theorem
computable.to₂
added
def
computable
added
theorem
computable₂.comp
added
theorem
computable₂.comp₂
added
theorem
computable₂.part
added
def
computable₂
added
theorem
nat.mem_rfind
added
theorem
nat.partrec.code.comp_prim
added
def
nat.partrec.code.encode_code
added
def
nat.partrec.code.eval
added
def
nat.partrec.code.evaln
added
theorem
nat.partrec.code.exists_code
added
def
nat.partrec.code.of_nat_code
added
theorem
nat.partrec.code.pair_prim
added
theorem
nat.partrec.code.prec_prim
added
theorem
nat.partrec.code.rec_prim
added
theorem
nat.partrec.code.rfind_prim
added
inductive
nat.partrec.code
added
theorem
nat.partrec.none
modified
theorem
nat.partrec.of_eq
added
theorem
nat.partrec.of_eq_tot
added
theorem
nat.partrec.of_primrec
added
theorem
nat.partrec.ppred
added
theorem
nat.partrec.prec'
deleted
theorem
nat.partrec.prim
added
theorem
nat.partrec.rfind'
added
def
nat.rfind
added
theorem
nat.rfind_dom'
added
theorem
nat.rfind_dom
added
theorem
nat.rfind_min'
added
theorem
nat.rfind_min
added
theorem
nat.rfind_spec
added
def
nat.rfind_x
added
theorem
nat.rfind_zero_none
added
theorem
partrec.comp
added
theorem
partrec.const'
added
theorem
partrec.map
added
theorem
partrec.nat_elim
added
theorem
partrec.nat_iff
added
theorem
partrec.none
added
theorem
partrec.of_eq
added
theorem
partrec.of_eq_tot
added
theorem
partrec.rfind
added
theorem
partrec.to₂
added
def
partrec
added
theorem
partrec₂.comp
added
theorem
partrec₂.comp₂
added
theorem
partrec₂.unpaired'
added
theorem
partrec₂.unpaired
added
def
partrec₂
added
theorem
primrec.to_comp
Modified
data/computability/primrec.lean
modified
theorem
nat.primrec.of_eq
modified
theorem
primrec.comp
added
theorem
primrec.list_concat
added
theorem
primrec.nat_strong_rec
modified
theorem
primrec.of_eq
modified
theorem
primrec₂.of_eq
Modified
data/denumerable.lean
added
def
equiv.list_equiv_self_of_equiv_nat
added
def
equiv.list_nat_equiv_nat
Modified
data/encodable.lean
added
theorem
encodable.decode_nat
added
theorem
encodable.encode_nat
Modified
data/equiv.lean
deleted
def
equiv.list_equiv_self_of_equiv_nat
deleted
def
equiv.list_nat_equiv_nat
Modified
data/nat/basic.lean
added
theorem
nat.bodd_bit0
added
theorem
nat.bodd_bit1
added
theorem
nat.div2_bit0
added
theorem
nat.div2_bit1
Modified
data/nat/pairing.lean
added
theorem
nat.le_mkpair_right
deleted
theorem
nat.unpair_le
added
theorem
nat.unpair_le_left
added
theorem
nat.unpair_le_right
Modified
data/pfun.lean
modified
theorem
pfun.bind_defined
added
theorem
pfun.dom_of_mem_fix
added
def
pfun.fix
added
theorem
pfun.mem_fix_iff
modified
def
pfun
deleted
def
roption.bind
added
theorem
roption.bind_map
added
theorem
roption.bind_none
modified
theorem
roption.bind_some_eq_map
added
theorem
roption.coe_none
added
theorem
roption.coe_some
modified
theorem
roption.dom_iff_mem
added
theorem
roption.eq_none_iff
added
theorem
roption.eq_some_iff
deleted
theorem
roption.eq_some_of_mem
added
theorem
roption.map_bind
added
theorem
roption.map_id'
added
theorem
roption.map_map
added
theorem
roption.map_none
added
theorem
roption.mem_assert
added
theorem
roption.mem_assert_iff
added
theorem
roption.not_mem_none
deleted
structure
roption
added
structure
{u}