Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-19 21:28 fc20442e

View on Github →

feat(computability/partrec): partial recursion, Godel numbering

Estimated changes

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 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 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
added theorem nat.bodd_bit0
added theorem nat.bodd_bit1
added theorem nat.div2_bit0
added theorem nat.div2_bit1
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}