Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-29 17:20 40bd9478

View on Github →

feat(computability/primrec): add traditional primrec definition This shows that the pairing function with its square roots does not give any additional power.

Estimated changes

added theorem nat.primrec'.add
added theorem nat.primrec'.comp'
added theorem nat.primrec'.comp₁
added theorem nat.primrec'.comp₂
added theorem nat.primrec'.const
added theorem nat.primrec'.head
added theorem nat.primrec'.idv
added theorem nat.primrec'.if_lt
added theorem nat.primrec'.mkpair
added theorem nat.primrec'.mul
added theorem nat.primrec'.of_eq
added theorem nat.primrec'.of_prim
added theorem nat.primrec'.prec'
added theorem nat.primrec'.pred
added theorem nat.primrec'.prim_iff
added theorem nat.primrec'.sqrt
added theorem nat.primrec'.sub
added theorem nat.primrec'.tail
added theorem nat.primrec'.to_prim
added theorem nat.primrec'.unpair₁
added theorem nat.primrec'.unpair₂
added inductive nat.primrec'
added theorem primrec.fin_app
added theorem primrec.fin_curry
added theorem primrec.fin_curry₁
added theorem primrec.fin_succ
added theorem primrec.fin_val
added theorem primrec.fin_val_iff
added theorem primrec.list_head'
added theorem primrec.list_head
added theorem primrec.list_of_fn
added theorem primrec.list_tail
added theorem primrec.nat_lt
added theorem primrec.nat_sqrt
added theorem primrec.of_equiv
added theorem primrec.of_equiv_iff
added theorem primrec.of_equiv_symm
added theorem primrec.subtype_val
added theorem primrec.vector_cons
added theorem primrec.vector_head
added theorem primrec.vector_length
added theorem primrec.vector_nth'
added theorem primrec.vector_nth
added theorem primrec.vector_of_fn'
added theorem primrec.vector_of_fn
added theorem primrec.vector_tail
added theorem primrec.vector_to_list
added def fin.cases
added theorem fin.cases_succ
added theorem fin.cases_zero
added theorem list.array_eq_of_fn
modified theorem list.cons_head_tail
added def list.head'
modified theorem list.head_append
modified theorem list.head_cons
added theorem list.head_eq_head'
added theorem list.length_of_fn
added theorem list.length_of_fn_aux
added theorem list.nth_le_of_fn
added theorem list.nth_of_fn
added theorem list.nth_of_fn_aux
added def list.of_fn
added def list.of_fn_aux
added theorem list.of_fn_nth_le
added theorem list.of_fn_succ
added theorem list.of_fn_zero
added theorem nat.eq_sqrt
modified theorem set.image_empty
modified theorem set.image_id
added theorem subtype.ext
added theorem subtype.val_injective
added theorem vector.head'_to_list
added theorem vector.head_of_fn
added theorem vector.mk_to_list
added theorem vector.nth_cons_succ
added theorem vector.nth_cons_zero
added theorem vector.nth_eq_nth_le
added theorem vector.nth_of_fn
added theorem vector.nth_tail
added theorem vector.nth_zero
added theorem vector.of_fn_nth
added theorem vector.tail_of_fn
added theorem vector.to_list_of_fn