Commit 2026-01-12 09:38 264da352

View on Github →

chore(Computability/Primrec): split file (#33835) This PR addresses an instance of the tech debt linter by splitting the file Computability/Primrec, currently the longest file in mathlib. It seems that most of the content after line 750 involves operations over Lists or List.Vectors (or that depend on operations over lists or vectors) and the earlier content does not, so this seems to be the place most natural to split.

Estimated changes

deleted def Nat.Primrec'.Vec
deleted theorem Nat.Primrec'.add
deleted theorem Nat.Primrec'.comp'
deleted theorem Nat.Primrec'.comp₁
deleted theorem Nat.Primrec'.comp₂
deleted theorem Nat.Primrec'.const
deleted theorem Nat.Primrec'.head
deleted theorem Nat.Primrec'.idv
deleted theorem Nat.Primrec'.if_lt
deleted theorem Nat.Primrec'.mul
deleted theorem Nat.Primrec'.natPair
deleted theorem Nat.Primrec'.of_eq
deleted theorem Nat.Primrec'.of_prim
deleted theorem Nat.Primrec'.prec'
deleted theorem Nat.Primrec'.pred
deleted theorem Nat.Primrec'.prim_iff
deleted theorem Nat.Primrec'.prim_iff₁
deleted theorem Nat.Primrec'.prim_iff₂
deleted theorem Nat.Primrec'.sqrt
deleted theorem Nat.Primrec'.sub
deleted theorem Nat.Primrec'.tail
deleted theorem Nat.Primrec'.to_prim
deleted theorem Nat.Primrec'.unpair₁
deleted theorem Nat.Primrec'.unpair₂
deleted theorem Nat.Primrec'.vec_iff
deleted inductive Nat.Primrec'
deleted theorem Nat.Primrec.add
deleted theorem Nat.Primrec.casesOn'
deleted theorem Nat.Primrec.casesOn1
deleted theorem Nat.Primrec.const
deleted theorem Nat.Primrec.mul
deleted theorem Nat.Primrec.of_eq
deleted theorem Nat.Primrec.pow
deleted theorem Nat.Primrec.prec1
deleted theorem Nat.Primrec.pred
deleted theorem Nat.Primrec.sub
deleted theorem Nat.Primrec.swap'
deleted def Nat.unpaired
deleted def Primcodable.ofEquiv
deleted def Primcodable.subtype
deleted theorem Primrec.bind_decode_iff
deleted theorem Primrec.comp
deleted theorem Primrec.comp₂
deleted theorem Primrec.cond
deleted theorem Primrec.const
deleted theorem Primrec.dom_bool
deleted theorem Primrec.dom_bool₂
deleted theorem Primrec.dom_denumerable
deleted theorem Primrec.dom_finite
deleted theorem Primrec.encdec
deleted theorem Primrec.encode_iff
deleted theorem Primrec.fin_app
deleted theorem Primrec.fin_curry
deleted theorem Primrec.fin_curry₁
deleted theorem Primrec.fin_succ
deleted theorem Primrec.fin_val
deleted theorem Primrec.fin_val_iff
deleted theorem Primrec.fst
deleted theorem Primrec.ite
deleted theorem Primrec.listFilter
deleted theorem Primrec.listFilterMap
deleted theorem Primrec.listLookup
deleted theorem Primrec.list_append
deleted theorem Primrec.list_casesOn
deleted theorem Primrec.list_concat
deleted theorem Primrec.list_cons
deleted theorem Primrec.list_findIdx
deleted theorem Primrec.list_findIdx₁
deleted theorem Primrec.list_flatMap
deleted theorem Primrec.list_flatten
deleted theorem Primrec.list_foldl
deleted theorem Primrec.list_foldr
deleted theorem Primrec.list_getD
deleted theorem Primrec.list_getElem?
deleted theorem Primrec.list_getElem?₁
deleted theorem Primrec.list_getI
deleted theorem Primrec.list_head?
deleted theorem Primrec.list_headI
deleted theorem Primrec.list_idxOf
deleted theorem Primrec.list_idxOf₁
deleted theorem Primrec.list_length
deleted theorem Primrec.list_map
deleted theorem Primrec.list_ofFn
deleted theorem Primrec.list_range
deleted theorem Primrec.list_rec
deleted theorem Primrec.list_reverse
deleted theorem Primrec.list_tail
deleted theorem Primrec.map_decode_iff
deleted theorem Primrec.nat_add
deleted theorem Primrec.nat_bodd
deleted theorem Primrec.nat_casesOn'
deleted theorem Primrec.nat_casesOn
deleted theorem Primrec.nat_casesOn₁
deleted theorem Primrec.nat_div2
deleted theorem Primrec.nat_div
deleted theorem Primrec.nat_double
deleted theorem Primrec.nat_double_succ
deleted theorem Primrec.nat_findGreatest
deleted theorem Primrec.nat_iff
deleted theorem Primrec.nat_iterate
deleted theorem Primrec.nat_le
deleted theorem Primrec.nat_lt
deleted theorem Primrec.nat_max
deleted theorem Primrec.nat_min
deleted theorem Primrec.nat_mod
deleted theorem Primrec.nat_mul
deleted theorem Primrec.nat_omega_rec'
deleted theorem Primrec.nat_omega_rec
deleted theorem Primrec.nat_rec'
deleted theorem Primrec.nat_rec
deleted theorem Primrec.nat_rec₁
deleted theorem Primrec.nat_sqrt
deleted theorem Primrec.nat_strong_rec
deleted theorem Primrec.nat_sub
deleted theorem Primrec.ofNat_iff
deleted theorem Primrec.of_eq
deleted theorem Primrec.of_equiv
deleted theorem Primrec.of_equiv_iff
deleted theorem Primrec.of_equiv_symm
deleted theorem Primrec.of_equiv_symm_iff
deleted theorem Primrec.of_graph
deleted theorem Primrec.optionToList
deleted theorem Primrec.option_bind
deleted theorem Primrec.option_bind₁
deleted theorem Primrec.option_casesOn
deleted theorem Primrec.option_get
deleted theorem Primrec.option_getD
deleted theorem Primrec.option_guard
deleted theorem Primrec.option_iget
deleted theorem Primrec.option_isSome
deleted theorem Primrec.option_map
deleted theorem Primrec.option_map₁
deleted theorem Primrec.option_orElse
deleted theorem Primrec.option_some
deleted theorem Primrec.option_some_iff
deleted theorem Primrec.pair
deleted theorem Primrec.pred
deleted theorem Primrec.primrecPred
deleted theorem Primrec.snd
deleted theorem Primrec.subtype_mk
deleted theorem Primrec.subtype_val
deleted theorem Primrec.subtype_val_iff
deleted theorem Primrec.succ
deleted theorem Primrec.sumCasesOn
deleted theorem Primrec.sumInl
deleted theorem Primrec.sumInr
deleted theorem Primrec.to₂
deleted theorem Primrec.ulower_down
deleted theorem Primrec.ulower_up
deleted theorem Primrec.unpair
deleted theorem Primrec.vector_cons
deleted theorem Primrec.vector_get'
deleted theorem Primrec.vector_get
deleted theorem Primrec.vector_head
deleted theorem Primrec.vector_length
deleted theorem Primrec.vector_ofFn'
deleted theorem Primrec.vector_ofFn
deleted theorem Primrec.vector_tail
deleted theorem Primrec.vector_toList
deleted theorem Primrec.vector_toList_iff
deleted def Primrec
deleted theorem PrimrecPred.comp
deleted theorem PrimrecPred.exists_lt
deleted theorem PrimrecPred.forall_lt
deleted theorem PrimrecPred.of_eq
deleted theorem PrimrecPred.primrecRel
deleted def PrimrecPred
deleted theorem PrimrecRel.comp
deleted theorem PrimrecRel.comp₂
deleted theorem PrimrecRel.exists_lt
deleted theorem PrimrecRel.forall_lt
deleted theorem PrimrecRel.listFilter
deleted theorem PrimrecRel.of_eq
deleted def PrimrecRel
deleted theorem Primrec₂.comp
deleted theorem Primrec₂.comp₂
deleted theorem Primrec₂.const
deleted theorem Primrec₂.curry
deleted theorem Primrec₂.encode_iff
deleted theorem Primrec₂.left
deleted theorem Primrec₂.mk
deleted theorem Primrec₂.natPair
deleted theorem Primrec₂.nat_iff'
deleted theorem Primrec₂.nat_iff
deleted theorem Primrec₂.ofNat_iff
deleted theorem Primrec₂.of_eq
deleted theorem Primrec₂.primrecRel
deleted theorem Primrec₂.right
deleted theorem Primrec₂.uncurry
deleted theorem Primrec₂.unpaired'
deleted theorem Primrec₂.unpaired
deleted def Primrec₂
added theorem Nat.Primrec.add
added theorem Nat.Primrec.casesOn'
added theorem Nat.Primrec.casesOn1
added theorem Nat.Primrec.const
added theorem Nat.Primrec.mul
added theorem Nat.Primrec.of_eq
added theorem Nat.Primrec.pow
added theorem Nat.Primrec.prec1
added theorem Nat.Primrec.pred
added theorem Nat.Primrec.sub
added theorem Nat.Primrec.swap'
added def Nat.unpaired
added theorem Primrec.comp
added theorem Primrec.comp₂
added theorem Primrec.cond
added theorem Primrec.const
added theorem Primrec.dom_bool
added theorem Primrec.dom_bool₂
added theorem Primrec.dom_finite
added theorem Primrec.encdec
added theorem Primrec.encode_iff
added theorem Primrec.fin_succ
added theorem Primrec.fin_val
added theorem Primrec.fin_val_iff
added theorem Primrec.fst
added theorem Primrec.ite
added theorem Primrec.list_idxOf₁
added theorem Primrec.map_decode_iff
added theorem Primrec.nat_add
added theorem Primrec.nat_bodd
added theorem Primrec.nat_casesOn'
added theorem Primrec.nat_casesOn
added theorem Primrec.nat_casesOn₁
added theorem Primrec.nat_div2
added theorem Primrec.nat_div
added theorem Primrec.nat_double
added theorem Primrec.nat_iff
added theorem Primrec.nat_iterate
added theorem Primrec.nat_le
added theorem Primrec.nat_lt
added theorem Primrec.nat_max
added theorem Primrec.nat_min
added theorem Primrec.nat_mod
added theorem Primrec.nat_mul
added theorem Primrec.nat_rec'
added theorem Primrec.nat_rec
added theorem Primrec.nat_rec₁
added theorem Primrec.nat_sub
added theorem Primrec.ofNat_iff
added theorem Primrec.of_eq
added theorem Primrec.of_equiv
added theorem Primrec.of_equiv_iff
added theorem Primrec.of_equiv_symm
added theorem Primrec.of_graph
added theorem Primrec.option_bind
added theorem Primrec.option_bind₁
added theorem Primrec.option_casesOn
added theorem Primrec.option_get
added theorem Primrec.option_getD
added theorem Primrec.option_guard
added theorem Primrec.option_iget
added theorem Primrec.option_isSome
added theorem Primrec.option_map
added theorem Primrec.option_map₁
added theorem Primrec.option_orElse
added theorem Primrec.option_some
added theorem Primrec.pair
added theorem Primrec.pred
added theorem Primrec.primrecPred
added theorem Primrec.snd
added theorem Primrec.subtype_mk
added theorem Primrec.subtype_val
added theorem Primrec.succ
added theorem Primrec.sumCasesOn
added theorem Primrec.sumInl
added theorem Primrec.sumInr
added theorem Primrec.to₂
added theorem Primrec.ulower_down
added theorem Primrec.ulower_up
added theorem Primrec.unpair
added def Primrec
added theorem PrimrecPred.comp
added theorem PrimrecPred.of_eq
added theorem PrimrecPred.primrecRel
added def PrimrecPred
added theorem PrimrecRel.comp
added theorem PrimrecRel.comp₂
added theorem PrimrecRel.of_eq
added def PrimrecRel
added theorem Primrec₂.comp
added theorem Primrec₂.comp₂
added theorem Primrec₂.const
added theorem Primrec₂.curry
added theorem Primrec₂.encode_iff
added theorem Primrec₂.left
added theorem Primrec₂.mk
added theorem Primrec₂.natPair
added theorem Primrec₂.nat_iff'
added theorem Primrec₂.nat_iff
added theorem Primrec₂.ofNat_iff
added theorem Primrec₂.of_eq
added theorem Primrec₂.primrecRel
added theorem Primrec₂.right
added theorem Primrec₂.uncurry
added theorem Primrec₂.unpaired'
added theorem Primrec₂.unpaired
added def Primrec₂
added def Nat.Primrec'.Vec
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'.mul
added theorem Nat.Primrec'.natPair
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 theorem Nat.Primrec'.vec_iff
added inductive Nat.Primrec'
added theorem Primrec.fin_app
added theorem Primrec.fin_curry
added theorem Primrec.fin_curry₁
added theorem Primrec.listFilter
added theorem Primrec.listFilterMap
added theorem Primrec.listLookup
added theorem Primrec.list_append
added theorem Primrec.list_casesOn
added theorem Primrec.list_concat
added theorem Primrec.list_cons
added theorem Primrec.list_findIdx
added theorem Primrec.list_flatMap
added theorem Primrec.list_flatten
added theorem Primrec.list_foldl
added theorem Primrec.list_foldr
added theorem Primrec.list_getD
added theorem Primrec.list_getElem?
added theorem Primrec.list_getI
added theorem Primrec.list_head?
added theorem Primrec.list_headI
added theorem Primrec.list_idxOf
added theorem Primrec.list_length
added theorem Primrec.list_map
added theorem Primrec.list_ofFn
added theorem Primrec.list_range
added theorem Primrec.list_rec
added theorem Primrec.list_reverse
added theorem Primrec.list_tail
added theorem Primrec.nat_omega_rec'
added theorem Primrec.nat_omega_rec
added theorem Primrec.nat_sqrt
added theorem Primrec.nat_strong_rec
added theorem Primrec.optionToList
added theorem Primrec.vector_cons
added theorem Primrec.vector_get'
added theorem Primrec.vector_get
added theorem Primrec.vector_head
added theorem Primrec.vector_length
added theorem Primrec.vector_ofFn'
added theorem Primrec.vector_ofFn
added theorem Primrec.vector_tail
added theorem Primrec.vector_toList
added theorem PrimrecPred.exists_lt
added theorem PrimrecPred.forall_lt
added theorem PrimrecRel.exists_lt
added theorem PrimrecRel.forall_lt
added theorem PrimrecRel.listFilter