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