Commit 2023-05-10 17:39 13d176b4

View on Github →

feat: port Computability.Halting (#3851)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/Halting.lean

added theorem ComputablePred.computable_iff

added theorem ComputablePred.computable_iff_re_compl_re'

added theorem ComputablePred.computable_iff_re_compl_re

added theorem ComputablePred.halting_problem

added theorem ComputablePred.halting_problem_not_re

added theorem ComputablePred.halting_problem_re

added theorem ComputablePred.of_eq

added theorem ComputablePred.rice

added theorem ComputablePred.rice₂

added theorem ComputablePred.to_re

added def ComputablePred

added def Nat.Partrec'.Vec

added theorem Nat.Partrec'.comp'

added theorem Nat.Partrec'.comp₁

added theorem Nat.Partrec'.head

added theorem Nat.Partrec'.idv

added theorem Nat.Partrec'.of_eq

added theorem Nat.Partrec'.of_part

added theorem Nat.Partrec'.of_prim

added theorem Nat.Partrec'.part_iff

added theorem Nat.Partrec'.part_iff₁

added theorem Nat.Partrec'.part_iff₂

added theorem Nat.Partrec'.rfindOpt

added theorem Nat.Partrec'.tail

added theorem Nat.Partrec'.to_part

added theorem Nat.Partrec'.vec_iff

added inductive Nat.Partrec'

added theorem Nat.Partrec.merge'

added theorem Partrec.cond

added theorem Partrec.dom_re

added theorem Partrec.merge'

added theorem Partrec.merge

added theorem RePred.of_eq

added def RePred

Modified Mathlib/Data/Part.lean