Commit 2023-05-10 11:05 5e04039c

View on Github →

feat: port Computability.PartrecCode (#3833) This PR also renames some decls in Computability.Primrec.

Estimated changes

added theorem Computable.ofOption
deleted theorem Computable.of_option
deleted theorem Computable.option_cases
deleted theorem Computable.sum_cases
added theorem Computable.sum_casesOn
deleted theorem Partrec.sum_cases_left
deleted theorem Partrec.sum_cases_right
added theorem Nat.Partrec.Code.smn
added inductive Nat.Partrec.Code
added theorem Nat.Partrec.rfind'
deleted theorem Nat.Primrec.cases1
deleted theorem Nat.Primrec.cases
added theorem Nat.Primrec.casesOn'
added theorem Nat.Primrec.casesOn1
deleted theorem Primrec.list_cases
added theorem Primrec.list_casesOn
deleted theorem Primrec.nat_cases'
deleted theorem Primrec.nat_cases
added theorem Primrec.nat_casesOn'
added theorem Primrec.nat_casesOn
added theorem Primrec.nat_casesOn₁
deleted theorem Primrec.nat_cases₁
deleted theorem Primrec.nat_elim'
deleted theorem Primrec.nat_elim
deleted theorem Primrec.nat_elim₁
added theorem Primrec.nat_rec'
added theorem Primrec.nat_rec
added theorem Primrec.nat_rec₁
deleted theorem Primrec.ofEquiv
deleted theorem Primrec.ofEquiv_iff
deleted theorem Primrec.ofEquiv_symm
deleted theorem Primrec.ofEquiv_symm_iff
added theorem Primrec.of_equiv
added theorem Primrec.of_equiv_iff
added theorem Primrec.of_equiv_symm
deleted theorem Primrec.option_cases
added theorem Primrec.option_casesOn
deleted theorem Primrec.sum_cases
added theorem Primrec.sum_casesOn
added theorem Primrec.vector_get'
deleted theorem Primrec.vector_nth'
added theorem Primrec.vector_ofFn'
deleted theorem Primrec.vector_of_fn'