Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2018-05-22 05:26
d62bf560
View on Github →
feat(computability/halting): halting problem
Estimated changes
Created
data/computability/halting.lean
added
theorem
computable_pred.halting_problem
added
theorem
computable_pred.of_eq
added
theorem
computable_pred.rice
added
theorem
computable_pred.rice₂
added
def
computable_pred
added
theorem
nat.partrec.merge'
added
theorem
partrec.cond
added
theorem
partrec.merge'
added
theorem
partrec.merge
added
theorem
partrec.sum_cases
added
def
re_pred
Modified
data/computability/partrec.lean
added
def
nat.rfind_opt
added
theorem
nat.rfind_opt_dom
added
theorem
nat.rfind_opt_mono
added
theorem
nat.rfind_opt_spec
added
theorem
partrec.bind_decode2_iff
added
theorem
partrec.map_encode_iff
added
theorem
partrec.rfind_opt
added
theorem
primrec₂.to_comp
Modified
data/computability/partrec_code.lean
added
theorem
nat.partrec.code.const_prim
added
def
nat.partrec.code.curry
added
theorem
nat.partrec.code.curry_prim
added
theorem
nat.partrec.code.eval_const
added
theorem
nat.partrec.code.eval_curry
added
theorem
nat.partrec.code.eval_id
added
theorem
nat.partrec.code.fixed_point
added
theorem
nat.partrec.code.fixed_point₂
Modified
data/computability/primrec.lean
added
theorem
primrec.option_guard
modified
theorem
primrec.option_is_some
added
theorem
primrec.option_orelse
Modified
data/encodable.lean
added
def
encodable.decode2
added
theorem
encodable.decode2_inj
added
theorem
encodable.encodek2
added
theorem
encodable.mem_decode2
Modified
data/option.lean
added
theorem
option.orelse_none'
added
theorem
option.orelse_none
added
theorem
option.orelse_some'
added
theorem
option.orelse_some
Modified
data/pfun.lean
added
theorem
roption.bind_some_right
added
theorem
roption.eq_none_iff'
added
theorem
roption.get_eq_of_mem
added
theorem
roption.get_mem