Partrec

📁 Source: Mathlib/Computability/Partrec.lean

Statistics

Metric	Count
Definitions Computable, Computable₂, Partrec, rfind, rfindOpt, rfindX, Partrec, Partrec₂	8
Theorems bind_decode_iff, comp, comp₂, cond, const, decode, encode, encode_iff, fin_app, fst, id, list_append, list_concat, list_cons, list_getElem?, list_length, list_ofFn, list_reverse, map_decode_iff, nat_bodd, nat_casesOn, nat_div2, nat_rec, nat_strong_rec, ofNat, ofOption, of_eq, option_bind, option_casesOn, option_getD, option_map, option_some, option_some_iff, pair, partrec, pred, snd, subtype_mk, succ, sumCasesOn, sumInl, sumInr, to₂, unpair, vector_cons, vector_get, vector_head, vector_length, vector_ofFn, vector_ofFn', vector_tail, vector_toList, comp, comp₂, mk, partrec₂, const', none, of_eq, of_eq_tot, of_primrec, ppred, prec', some, mem_rfind, rfindOpt_dom, rfindOpt_mono, rfindOpt_spec, rfind_dom, rfind_dom', rfind_min, rfind_min', rfind_spec, rfind_zero_none, bind, bind_decode₂_iff, comp, const', fix, fix_aux, map, map_encode_iff, nat_casesOn_right, nat_iff, nat_rec, none, of_eq, of_eq_tot, optionCasesOn_right, option_some_iff, rfind, rfindOpt, some, sumCasesOn_left, sumCasesOn_right, to₂, vector_mOfFn, comp, comp₂, unpaired, unpaired', to_comp, to_comp, mOfFn_part_some	104
Total	112

Computable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bind_decode_iff 📖	mathematical	—	Computable₂ Primcodable.ofDenumerable Denumerable.nat Primcodable.option Encodable.decode Primcodable.toEncodable	—	Nat.Partrec.of_eq Partrec.bind Partrec.comp Partrec.nat_iff Nat.Partrec.ppred Primcodable.prim snd Computable₂.partrec₂ to₂ comp fst Encodable.decode_prod_val Option.bind_congr' Part.bind_some Part.map_bind Part.map_some Part.bind_none Partrec.nat_casesOn_right Primrec.to_comp Primrec.encdec const Partrec.map ofOption decode Computable₂.comp Partrec.of_eq Encodable.encodek
comp 📖	—	Computable	—	—	Partrec.comp
comp₂ 📖	—	Computable Computable₂	—	—	comp
cond 📖	—	Computable Primcodable.bool	—	—	of_eq encode_iff to₂ comp fst
const 📖	mathematical	—	Computable	—	Primrec.to_comp Primrec.const
decode 📖	mathematical	—	Computable Primcodable.ofDenumerable Denumerable.nat Primcodable.option Encodable.decode Primcodable.toEncodable	—	Primrec.to_comp Primrec.decode
encode 📖	mathematical	—	Computable Primcodable.ofDenumerable Denumerable.nat Encodable.encode Primcodable.toEncodable	—	Primrec.to_comp Primrec.encode
encode_iff 📖	mathematical	—	Computable Primcodable.ofDenumerable Denumerable.nat Encodable.encode Primcodable.toEncodable	—	—
fin_app 📖	mathematical	—	Computable₂ Primcodable.finArrow Primcodable.fin	—	Primrec₂.to_comp Primrec.fin_app
fst 📖	mathematical	—	Computable Primcodable.prod	—	Primrec.to_comp Primrec.fst
id 📖	mathematical	—	Computable	—	Primrec.to_comp Primrec.id
list_append 📖	mathematical	—	Computable₂ Primcodable.list	—	Primrec₂.to_comp Primrec.list_append
list_concat 📖	mathematical	—	Computable₂ Primcodable.list	—	Primrec₂.to_comp Primrec.list_concat
list_cons 📖	mathematical	—	Computable₂ Primcodable.list	—	Primrec₂.to_comp Primrec.list_cons
list_getElem? 📖	mathematical	—	Computable₂ Primcodable.list Primcodable.ofDenumerable Denumerable.nat Primcodable.option	—	Primrec₂.to_comp Primrec.list_getElem?
list_length 📖	mathematical	—	Computable Primcodable.list Primcodable.ofDenumerable Denumerable.nat	—	Primrec.to_comp Primrec.list_length
list_ofFn 📖	mathematical	Computable	Primcodable.list	—	const Computable₂.comp list_cons
list_reverse 📖	mathematical	—	Computable Primcodable.list	—	Primrec.to_comp Primrec.list_reverse
map_decode_iff 📖	mathematical	—	Computable₂ Primcodable.ofDenumerable Denumerable.nat Primcodable.option Encodable.decode Primcodable.toEncodable	—	bind_decode_iff option_some_iff
nat_bodd 📖	mathematical	—	Computable Primcodable.ofDenumerable Denumerable.nat Primcodable.bool Nat.bodd	—	Primrec.to_comp Primrec.nat_bodd
nat_casesOn 📖	—	Computable Primcodable.ofDenumerable Denumerable.nat Computable₂	—	—	to₂ Computable₂.comp fst comp snd
nat_div2 📖	mathematical	—	Computable Primcodable.ofDenumerable Denumerable.nat Nat.div2	—	Primrec.to_comp Primrec.nat_div2
nat_rec 📖	—	Computable Primcodable.ofDenumerable Denumerable.nat Computable₂ Primcodable.prod	—	—	Partrec.of_eq Computable₂.partrec₂ Part.bind_some
nat_strong_rec 📖	mathematical	Computable₂ Primcodable.list Primcodable.option	Primcodable.ofDenumerable Denumerable.nat	—	option_some_iff of_eq snd const to₂ option_bind comp option_map Computable₂.comp fst list_concat Option.bind_congr' list_getElem? succ IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass
ofNat 📖	mathematical	—	Computable Primcodable.ofDenumerable Denumerable.nat Denumerable.ofNat	—	Primrec.to_comp Primrec.ofNat
ofOption 📖	mathematical	Computable Primcodable.option	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	—	Nat.Partrec.of_eq Nat.Partrec.ppred Part.map_some Part.bind_none Part.bind_some Part.map_none
of_eq 📖	—	Computable	—	—	—
option_bind 📖	—	Computable Primcodable.option Computable₂	—	—	of_eq const
option_casesOn 📖	—	Computable Primcodable.option Computable₂	—	—	option_some_iff of_eq encode_iff map_decode_iff Encodable.encodek
option_getD 📖	—	Computable Primcodable.option	—	—	of_eq snd
option_map 📖	—	Computable Primcodable.option Computable₂	—	—	option_bind comp₂ option_some
option_some 📖	mathematical	—	Computable Primcodable.option	—	Primrec.to_comp Primrec.option_some
option_some_iff 📖	mathematical	—	Computable Primcodable.option	—	encode_iff comp Primrec.to_comp Primrec.pred option_some
pair 📖	mathematical	Computable	Primcodable.prod	—	Nat.Partrec.of_eq Part.map_some Part.bind_none Part.map_none Part.bind_some
partrec 📖	mathematical	Computable	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode PFun.lift	—	—
pred 📖	mathematical	—	Computable Primcodable.ofDenumerable Denumerable.nat	—	Primrec.to_comp Primrec.pred
snd 📖	mathematical	—	Computable Primcodable.prod	—	Primrec.to_comp Primrec.snd
subtype_mk 📖	mathematical	PrimrecPred Computable	Primcodable.subtype	—	—
succ 📖	mathematical	—	Computable Primcodable.ofDenumerable Denumerable.nat	—	Primrec.to_comp Primrec.succ
sumCasesOn 📖	—	Computable Primcodable.sum Computable₂	—	—	option_some_iff of_eq cond comp nat_bodd encode_iff option_map decode nat_div2 Nat.bodd_mul Nat.bodd_succ Nat.div2_val mul_div_cancel_left₀ Nat.instMulDivCancelClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat Encodable.encodek Nat.div2_succ
sumInl 📖	mathematical	—	Computable Primcodable.sum	—	Primrec.to_comp Primrec.sumInl
sumInr 📖	mathematical	—	Computable Primcodable.sum	—	Primrec.to_comp Primrec.sumInr
to₂ 📖	mathematical	Computable Primcodable.prod	Computable₂	—	of_eq
unpair 📖	mathematical	—	Computable Primcodable.ofDenumerable Denumerable.nat Primcodable.prod Nat.unpair	—	Primrec.to_comp Primrec.unpair
vector_cons 📖	mathematical	—	Computable₂ List.Vector Primcodable.vector List.Vector.cons	—	Primrec₂.to_comp Primrec.vector_cons
vector_get 📖	mathematical	—	Computable₂ List.Vector Primcodable.vector Primcodable.fin List.Vector.get	—	Primrec₂.to_comp Primrec.vector_get
vector_head 📖	mathematical	—	Computable List.Vector Primcodable.vector List.Vector.head	—	Primrec.to_comp Primrec.vector_head
vector_length 📖	mathematical	—	Computable List.Vector Primcodable.vector Primcodable.ofDenumerable Denumerable.nat List.Vector.length	—	Primrec.to_comp Primrec.vector_length
vector_ofFn 📖	mathematical	Computable	List.Vector Primcodable.vector List.Vector.ofFn	—	Partrec.of_eq Partrec.vector_mOfFn Vector.mOfFn_part_some
vector_ofFn' 📖	mathematical	—	Computable List.Vector Primcodable.finArrow Primcodable.vector List.Vector.ofFn	—	Primrec.to_comp Primrec.vector_ofFn'
vector_tail 📖	mathematical	—	Computable List.Vector Primcodable.vector List.Vector.tail	—	Primrec.to_comp Primrec.vector_tail
vector_toList 📖	mathematical	—	Computable List.Vector Primcodable.vector Primcodable.list List.Vector.toList	—	Primrec.to_comp Primrec.vector_toList

Computable₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	Computable₂ Computable	—	—	Computable.comp Computable.pair
comp₂ 📖	—	Computable₂	—	—	comp
mk 📖	mathematical	Computable Primcodable.prod	Computable₂	—	—
partrec₂ 📖	mathematical	Computable₂	Partrec₂ PFun.lift	—	—

Decidable.Partrec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const' 📖	mathematical	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	—	Partrec.of_eq Computable.ofOption Computable.const Part.of_toOption

Nat

Definitions

Name	Category	Theorems
Partrec 📖	CompData	—
rfind 📖	CompOp	6 math math: rfind_zero_none, rfind_dom, rfind_min', mem_rfind, Partrec.rfind', rfind_dom'
rfindOpt 📖	CompOp	4 math math: rfindOpt_dom, rfindOpt_mono, Partrec.Code.eval_eq_rfindOpt, Partrec'.rfindOpt
rfindX 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_rfind 📖	mathematical	—	Part Part.instMembership rfind	—	rfind_spec rfind_min Part.dom_iff_mem rfind_dom Exists.fst lt_trichotomy Part.mem_unique
rfindOpt_dom 📖	mathematical	—	Part.Dom rfindOpt	—	rfindOpt_spec find_spec rfind_spec Part.get_mem
rfindOpt_mono 📖	mathematical	—	Part Part.instMembership rfindOpt	—	rfindOpt_spec rfindOpt_dom le_max_left le_max_right
rfindOpt_spec 📖	—	Part Part.instMembership rfindOpt	—	—	Part.mem_bind_iff Part.mem_coe
rfind_dom 📖	mathematical	—	Part.Dom rfind Part Part.instMembership	—	—
rfind_dom' 📖	mathematical	—	Part.Dom rfind Part Part.instMembership	—	Decidable.eq_or_lt_of_le Exists.fst le_of_lt
rfind_min 📖	—	Part Part.instMembership rfind	—	—	Exists.fst Exists.snd
rfind_min' 📖	mathematical	—	Part Part.instMembership rfind PFun.lift	—	Part.dom_iff_mem rfind_dom not_lt Part.mem_unique rfind_min
rfind_spec 📖	—	Part Part.instMembership rfind	—	—	Exists.fst Exists.snd
rfind_zero_none 📖	mathematical	Part.none	rfind	—	Part.eq_none_iff rfind_dom' Exists.fst

Nat.Partrec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
none 📖	mathematical	—	Part.none	—	of_eq Nat.Primrec.const Part.eq_none_iff Part.map_some
of_eq 📖	—	—	—	—	—
of_eq_tot 📖	mathematical	Part Part.instMembership	PFun.lift	—	of_eq Part.eq_some_iff
of_primrec 📖	mathematical	—	PFun.lift	—	of_eq_tot Part.map_some Part.bind_some
ppred 📖	mathematical	—	Part.ofOption Nat.ppred	—	Primrec.to₂ Primrec.ite PrimrecRel.comp Primrec.eq Primrec.fst Primrec.comp Primrec.succ Primrec.snd Primrec.const of_eq Primrec₂.unpaired' Nat.unpair_pair Part.map_some Part.eq_none_iff Part.eq_some_iff
prec' 📖	mathematical	—	Part.bind Part Part.instMonad Nat.pair	—	of_eq some Part.ext Part.map_some Part.bind_some Part.bind_map Nat.unpair_pair
some 📖	mathematical	—	Part.some	—	Nat.Primrec.id

Partrec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bind 📖	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode Partrec₂	—	—	Nat.Partrec.of_eq Nat.Partrec.some Part.map_some Part.map_bind Part.bind_some Encodable.decode_prod_val Part.bind_none Part.bind_map Option.bind_congr' Nat.unpair_pair Encodable.encodek
bind_decode₂_iff 📖	mathematical	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode Encodable.decode₂	—	nat_iff bind Computable.ofOption Primrec.to_comp Primrec.decode₂ comp map Computable.to₂ Computable.comp Computable.encode Computable.snd map_encode_iff Encodable.decode₂_encode Part.bind_some
comp 📖	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode Computable	—	—	Nat.Partrec.of_eq Part.map_some Part.bind_none Part.bind_some Encodable.encodek
const' 📖	mathematical	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	—	Decidable.Partrec.const'
fix 📖	mathematical	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode Primcodable.sum	PFun.fix	—	Computable.snd Computable.comp Computable.sumInr Computable.fst to₂ sumCasesOn_right Computable.to₂ comp map Computable.sumCasesOn Computable.id Computable.const of_eq bind rfind none Part.ext fix_aux
fix_aux 📖	mathematical	—	Part Part.instMembership PFun.fix	—	PFun.mem_fix_iff Part.mem_unique le_antisymm
map 📖	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode Computable₂	—	—	Part.bind_some_eq_map bind
map_encode_iff 📖	mathematical	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode Primcodable.ofDenumerable Denumerable.nat	—	—
nat_casesOn_right 📖	mathematical	Computable Primcodable.ofDenumerable Denumerable.nat Partrec₂	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	—	of_eq to₂ Partrec₂.comp Computable.fst Computable.comp Computable.pred Nat.instCanonicallyOrderedAdd add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Part.ext Part.mem_bind_iff Exists.fst Exists.snd
nat_iff 📖	mathematical	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Primcodable.ofDenumerable Denumerable.nat Part.map Encodable.encode	—	Part.map_id' Part.bind_some
nat_rec 📖	—	Computable Primcodable.ofDenumerable Denumerable.nat Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode Partrec₂ Primcodable.prod	—	—	Nat.Partrec.of_eq Nat.Partrec.prec' Part.map_some Part.bind_none Encodable.decode_prod_val Option.bind_congr' Nat.unpair_pair Part.bind_some Part.map_bind Part.bind_map Encodable.encodek
none 📖	mathematical	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	—	Nat.Partrec.of_eq Nat.Partrec.none Part.map_none Part.bind_none Part.bind_some
of_eq 📖	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	—	—	—
of_eq_tot 📖	mathematical	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode Part Part.instMembership	Computable	—	of_eq Part.eq_some_iff
optionCasesOn_right 📖	mathematical	Computable Primcodable.option Partrec₂	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	—	nat_casesOn_right Computable.encode_iff bind Computable.ofOption Computable.comp Computable.decode Computable.snd to₂ Partrec₂.comp Computable.fst of_eq Encodable.encodek Part.bind_some
option_some_iff 📖	mathematical	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode Primcodable.option	—	Nat.Partrec.of_eq Nat.Partrec.ppred Part.bind_assoc Part.bind_map Part.bind_some_eq_map map Computable.to₂ Computable.comp Computable.option_some Computable.snd
rfind 📖	mathematical	Partrec₂ Primcodable.ofDenumerable Denumerable.nat Primcodable.bool	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	—	Nat.Partrec.of_eq map Primrec₂.to_comp Primrec.to₂ Primrec.comp Primrec.dom_bool Primrec.snd Encodable.decode_prod_val Option.bind_congr' Nat.unpair_pair Part.map_id' Part.bind_none Part.map_none Nat.rfind_zero_none Part.bind_some Part.map_map
rfindOpt 📖	mathematical	Computable₂ Primcodable.ofDenumerable Denumerable.nat Primcodable.option	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	—	bind rfind to₂ Computable.comp Primrec.to_comp Primrec.option_isSome Computable.ofOption
some 📖	mathematical	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode Part.some	—	Computable.id
sumCasesOn_left 📖	mathematical	Computable Primcodable.sum Partrec₂ Computable₂	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	—	of_eq sumCasesOn_right Computable.sumCasesOn Computable.to₂ Computable.comp Computable.sumInr Computable.snd Computable.sumInl
sumCasesOn_right 📖	mathematical	Computable Primcodable.sum Computable₂ Partrec₂	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	—	optionCasesOn_right Computable.sumCasesOn Computable.to₂ Computable.const Computable.comp Computable.option_some Computable.snd option_some_iff of_eq Part.map_some
to₂ 📖	mathematical	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Primcodable.prod Part.map Encodable.encode	Partrec₂	—	of_eq
vector_mOfFn 📖	mathematical	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	List.Vector Primcodable.vector	—	Computable.const bind comp Computable.fst Computable₂.comp Primrec₂.to_comp Primrec.vector_cons Computable.comp Computable.snd

Partrec₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	Partrec₂ Computable	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode	—	Partrec.comp Computable.pair
comp₂ 📖	—	Partrec₂ Computable₂	—	—	comp
unpaired 📖	mathematical	—	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Primcodable.ofDenumerable Denumerable.nat Part.map Encodable.encode Nat.unpaired Part Partrec₂	—	Partrec.comp Primrec₂.to_comp Primrec₂.pair Primrec.to_comp Primrec.unpair
unpaired' 📖	mathematical	—	Nat.unpaired Part Partrec₂ Primcodable.ofDenumerable Denumerable.nat	—	Partrec.nat_iff unpaired

Primrec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_comp 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Encodable.decode	Computable	—	Nat.Partrec.of_eq Nat.Partrec.ppred Part.bind_some Part.map_some Part.bind_none

Primrec₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_comp 📖	mathematical	Primrec₂	Computable₂	—	Primrec.to_comp

Vector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mOfFn_part_some 📖	mathematical	—	List.Vector.mOfFn Part Part.instMonad Part.some List.Vector List.Vector.ofFn	—	List.Vector.mOfFn_pure Part.instLawfulMonad

(root)

Definitions

Name	Category	Theorems
Computable 📖	MathDef	31 math math: ComputablePred.decide, Computable.encode_iff, computablePred_iff_computable_decide, Computable.list_reverse, Computable.encode, Computable.ofNat, Computable.decode, Primrec.to_comp, Computable.sumInr, Nat.Partrec.Code.instCountableSubtypeForallComputable, Computable.option_some_iff, Computable.snd, Computable.sumInl, Computable.vector_ofFn', Computable.unpair, Computable.vector_head, Computable.list_length, Nat.Partrec'.vec_iff, Computable.option_some, Computable.vector_toList, Computable.vector_length, Computable.succ, Computable.fst, Computable.nat_div2, Partrec.of_eq_tot, Computable.const, ComputablePred.computable_iff, Computable.pred, Computable.nat_bodd, Computable.vector_tail, Computable.id
Computable₂ 📖	MathDef	14 math math: Computable.vector_cons, Computable.list_getElem?, Computable.list_cons, Computable.list_concat, Computable₂.mk, Computable.bind_decode_iff, Computable.map_decode_iff, Computable.list_append, Nat.Partrec.Code.smn, Computable.vector_get, computable₂_ack, Computable.to₂, Primrec₂.to_comp, Computable.fin_app
Partrec 📖	MathDef	—
Partrec₂ 📖	MathDef	6 math math: Computable₂.partrec₂, Partrec₂.unpaired', Partrec.to₂, Nat.Partrec.Code.eval_part, Nat.Partrec'.part_iff₂, Partrec₂.unpaired

---

← Back to Index