Commit 2023-05-08 03:07 da8157c6

View on Github →

feat: port Computability.Partrec (#3830)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/Partrec.lean

added theorem Computable.bind_decode_iff

added theorem Computable.comp₂

added theorem Computable.cond

added theorem Computable.const

added theorem Computable.encode_iff

added theorem Computable.fin_app

added theorem Computable.fst

added theorem Computable.list_append

added theorem Computable.list_concat

added theorem Computable.list_cons

added theorem Computable.list_get?

added theorem Computable.list_length

added theorem Computable.list_ofFn

added theorem Computable.list_reverse

added theorem Computable.map_decode_iff

added theorem Computable.nat_bodd

added theorem Computable.nat_casesOn

added theorem Computable.nat_div2

added theorem Computable.nat_rec

added theorem Computable.nat_strong_rec

added theorem Computable.of_eq

added theorem Computable.of_option

added theorem Computable.option_bind

added theorem Computable.option_cases

added theorem Computable.option_getD

added theorem Computable.option_map

added theorem Computable.option_some

added theorem Computable.option_some_iff

added theorem Computable.pred

added theorem Computable.snd

added theorem Computable.subtype_mk

added theorem Computable.succ

added theorem Computable.sum_cases

added theorem Computable.sum_inl

added theorem Computable.sum_inr

added theorem Computable.to₂

added theorem Computable.unpair

added theorem Computable.vector_cons

added theorem Computable.vector_get

added theorem Computable.vector_head

added theorem Computable.vector_length

added theorem Computable.vector_ofFn'

added theorem Computable.vector_ofFn

added theorem Computable.vector_tail

added theorem Computable.vector_toList

added def Computable

added theorem Computable₂.comp₂

added def Computable₂

added theorem Decidable.Partrec.const'

added theorem Nat.Partrec.none

added theorem Nat.Partrec.of_eq

added theorem Nat.Partrec.of_eq_tot

added theorem Nat.Partrec.of_primrec

added theorem Nat.Partrec.ppred

added theorem Nat.Partrec.prec'

added inductive Nat.Partrec

added theorem Nat.mem_rfind

added def Nat.rfind

added def Nat.rfindOpt

added theorem Nat.rfindOpt_dom

added theorem Nat.rfindOpt_mono

added theorem Nat.rfindOpt_spec

added def Nat.rfindX

added theorem Nat.rfind_dom'

added theorem Nat.rfind_dom

added theorem Nat.rfind_min'

added theorem Nat.rfind_min

added theorem Nat.rfind_spec

added theorem Nat.rfind_zero_none

added theorem Partrec.bind_decode₂_iff

added theorem Partrec.const'

added theorem Partrec.fix

added theorem Partrec.fix_aux

added theorem Partrec.map

added theorem Partrec.map_encode_iff

added theorem Partrec.nat_casesOn_right

added theorem Partrec.nat_iff

added theorem Partrec.nat_rec

added theorem Partrec.none

added theorem Partrec.of_eq

added theorem Partrec.of_eq_tot

added theorem Partrec.option_cases_right

added theorem Partrec.option_some_iff

added theorem Partrec.rfind

added theorem Partrec.rfindOpt

added theorem Partrec.sum_cases_left

added theorem Partrec.sum_cases_right

added theorem Partrec.to₂

added theorem Partrec.vector_mOfFn

added def Partrec

added theorem Partrec₂.comp₂

added theorem Partrec₂.unpaired'

added theorem Partrec₂.unpaired

added def Partrec₂

added theorem Primrec.to_comp

added theorem Vector.mOfFn_part_some