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

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}