Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-30 15:29 bdd54acd

View on Github →

feat(data/computablility): reduced partrec

Estimated changes

Modified data/computability/halting.lean

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'.rfind_opt

added theorem nat.partrec'.tail

added theorem nat.partrec'.to_part

added theorem nat.partrec'.vec.prim

added def nat.partrec'.vec

added theorem nat.partrec'.vec_iff

added inductive nat.partrec'

Modified data/computability/partrec.lean

added theorem computable.fin_app

added theorem computable.list_of_fn

added theorem computable.vector_cons

added theorem computable.vector_head

added theorem computable.vector_length

added theorem computable.vector_nth'

added theorem computable.vector_nth

added theorem computable.vector_of_fn'

added theorem computable.vector_of_fn

added theorem computable.vector_tail

added theorem computable.vector_to_list

added theorem partrec.vector_m_of_fn

added theorem vector.m_of_fn_roption_some

Modified data/computability/partrec_code.lean

added theorem nat.partrec.code.eval_eq_rfind_opt

Modified data/computability/primrec.lean

modified theorem nat.primrec'.idv

deleted def nat.primrec'.primvec

deleted theorem nat.primrec'.primvec_iff

added def nat.primrec'.vec

added theorem nat.primrec'.vec_iff

Modified data/vector2.lean

added theorem vector.m_of_fn_pure

added theorem vector.mmap_cons

added theorem vector.mmap_nil

added def vector.{u}