Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-18 05:10 92feaf95

View on Github →

feat(computability/primrec): list definitions are primrec

Estimated changes

added theorem primrec.list_append
added theorem primrec.list_cases
added theorem primrec.list_cons
modified theorem primrec.list_find_index
added theorem primrec.list_foldl
added theorem primrec.list_foldr
modified theorem primrec.list_index_of
modified theorem primrec.list_inth
added theorem primrec.list_join
added theorem primrec.list_length
added theorem primrec.list_map
modified theorem primrec.list_nth
added theorem primrec.list_nth₁
added theorem primrec.list_rec
added theorem primrec.list_reverse
deleted theorem primrec.nat_cases1
added theorem primrec.nat_cases₁
deleted theorem primrec.nat_elim1
added theorem primrec.nat_elim₁
added theorem primrec.nat_iterate
deleted theorem primrec.option_bind1
added theorem primrec.option_bind₁
deleted theorem primrec.option_map1
added theorem primrec.option_map₁
added theorem primrec.sum_cases
added theorem primrec.sum_inl
added theorem primrec.sum_inr
added theorem primrec.to₂
added theorem encodable.encode_inl
added theorem encodable.encode_inr
added theorem list.drop_nil
deleted def nat.foldl
deleted def nat.foldr
added theorem nat.iterate_add
added theorem nat.iterate_succ'
added theorem nat.iterate_succ
added theorem nat.iterate_zero
added theorem nat.le_mkpair_left
modified def nat.mkpair
modified theorem nat.mkpair_unpair
modified def nat.unpair
modified theorem nat.unpair_le
modified theorem nat.unpair_lt
modified theorem nat.unpair_mkpair
deleted theorem ordinal.foldr_le_nfp
added theorem ordinal.iterate_le_nfp