List

📁 Source: Mathlib/Computability/Primrec/List.lean

Statistics

Metric	Count
Definitions Primrec', finArrow, list, vector	4
Theorems add, comp', comp₁, comp₂, cons, const, encode, head, idv, if_lt, mul, natPair, nil, of_eq, of_prim, prec', pred, prim_iff, prim_iff₁, prim_iff₂, sub, tail, to_prim, unpair₁, unpair₂, vec_iff, fin_app, fin_curry, fin_curry₁, listFilter, listFilterMap, listLookup, list_append, list_casesOn, list_concat, list_cons, list_findIdx, list_flatMap, list_flatten, list_foldl, list_foldr, list_getD, list_getElem?, list_getI, list_head?, list_headI, list_idxOf, list_length, list_map, list_ofFn, list_range, list_rec, list_reverse, list_tail, nat_omega_rec, nat_omega_rec', nat_sqrt, nat_strong_rec, optionToList, vector_cons, vector_get, vector_get', vector_head, vector_length, vector_ofFn, vector_ofFn', vector_tail, vector_toList, vector_toList_iff, exists_lt, exists_mem_list, forall_lt, forall_mem_list, listFilter_listRange, exists_lt, exists_mem_list, forall_lt, forall_mem_list, listFilter	79
Total	83

Nat

Definitions

Name	Category	Theorems
Primrec' 📖	CompData	13 math math: Primrec'.sub, Primrec'.encode, Primrec'.natPair, Primrec'.pred, Primrec'.head, Primrec'.prim_iff₂, Primrec'.prim_iff, Primrec'.add, Primrec'.of_prim, Primrec'.prim_iff₁, Primrec'.mul, Primrec'.sqrt, Primrec'.const

Nat.Primrec'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	—	Nat.Primrec' List.Vector.head List.Vector.tail	—	of_eq head comp₁ tail List.Vector.tail_cons List.Vector.head_cons zero_add
comp' 📖	—	Nat.Primrec' Vec	—	—	of_eq List.Vector.ofFn_get
comp₁ 📖	—	Nat.Primrec' List.Vector.head	—	—	—
comp₂ 📖	—	Nat.Primrec' List.Vector.head List.Vector.tail	—	—	List.Vector.head_cons List.Vector.tail_cons comp' cons nil
cons 📖	mathematical	Nat.Primrec' Vec	List.Vector.cons	—	List.Vector.get_zero List.Vector.head_cons List.Vector.get_cons_succ
const 📖	mathematical	—	Nat.Primrec'	—	—
encode 📖	mathematical	—	Nat.Primrec' Encodable.encode List.Vector Encodable.List.Vector.encodable Nat.encodable	—	of_eq const List.Vector.eq_nil comp₁ comp₂ natPair head tail
head 📖	mathematical	—	Nat.Primrec' List.Vector.head	—	of_eq List.Vector.get_zero
idv 📖	mathematical	—	Vec List.Vector	—	—
if_lt 📖	—	Nat.Primrec'	—	—	of_eq prec' comp₂ sub tail List.Vector.tail_cons not_lt
mul 📖	mathematical	—	Nat.Primrec' List.Vector.head List.Vector.tail	—	of_eq const tail comp₂ add head List.Vector.tail_cons List.Vector.head_cons MulZeroClass.zero_mul add_comm
natPair 📖	mathematical	—	Nat.Primrec' Nat.pair List.Vector.head List.Vector.tail	—	if_lt head tail comp₂ add mul
nil 📖	mathematical	—	Vec List.Vector.nil	—	—
of_eq 📖	—	Nat.Primrec'	—	—	—
of_prim 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable Denumerable.nat List.Vector Encodable.decode Primcodable.vector	Nat.Primrec'	—	const unpair₁ head unpair₂ comp₂ natPair comp₁ List.Vector.tail_cons List.Vector.head_cons prec' tail of_eq pred encode Encodable.encodek add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
prec' 📖	mathematical	Nat.Primrec'	List.Vector.cons	—	List.Vector.tail_cons List.Vector.head_cons comp' cons idv
pred 📖	mathematical	—	Nat.Primrec' List.Vector.head	—	of_eq prec' head const List.Vector.head_cons
prim_iff 📖	mathematical	—	Nat.Primrec' Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable Denumerable.nat List.Vector Encodable.decode Primcodable.vector	—	to_prim of_prim
prim_iff₁ 📖	mathematical	—	Nat.Primrec' List.Vector.head Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable Denumerable.nat Encodable.decode	—	prim_iff Primrec.of_eq Primrec.comp Primrec.vector_ofFn Primrec.id List.Vector.head_ofFn Primrec.vector_head
prim_iff₂ 📖	mathematical	—	Nat.Primrec' List.Vector.head List.Vector.tail Primrec₂ Primcodable.ofDenumerable Denumerable.nat	—	prim_iff Primrec.of_eq Primrec.comp Primrec₂.comp Primrec.vector_cons Primrec.fst Primrec.snd Primrec.const List.Vector.head_cons List.Vector.tail_cons Primrec.vector_head Primrec.vector_tail
sub 📖	mathematical	—	Nat.Primrec' List.Vector.head List.Vector.tail	—	of_eq head comp₁ pred tail List.Vector.tail_cons List.Vector.head_cons tsub_zero Nat.instOrderedSub comp₂
tail 📖	mathematical	Nat.Primrec'	List.Vector.tail	—	of_eq List.Vector.ofFn_get List.Vector.get_tail_succ
to_prim 📖	mathematical	Nat.Primrec'	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable Denumerable.nat List.Vector Encodable.decode Primcodable.vector	—	Primrec.const Primrec.comp Primrec.succ Primrec.vector_head Primrec₂.comp Primrec.vector_get Primrec.id Primrec.vector_ofFn Primrec.nat_rec' Primrec.vector_tail Primrec.to₂ Primrec.vector_cons Primrec.fst Primrec.snd
unpair₁ 📖	mathematical	Nat.Primrec'	Nat.unpair	—	comp₁ sqrt comp₂ sub mul of_eq if_lt
unpair₂ 📖	mathematical	Nat.Primrec'	Nat.unpair	—	comp₁ sqrt comp₂ sub mul of_eq if_lt
vec_iff 📖	mathematical	—	Vec Encodable.encode List.Vector Option.encodable Primcodable.toEncodable Primcodable.vector Primcodable.ofDenumerable Denumerable.nat Encodable.decode	—	List.Vector.ofFn_get Primrec.vector_ofFn to_prim of_prim Primrec₂.comp Primrec.vector_get Primrec.const

Primcodable

Definitions

Name	Category	Theorems
finArrow 📖	CompOp	6 math math: Primrec.vector_ofFn', Computable.vector_ofFn', Primrec.fin_curry, Primrec.vector_get', Primrec.fin_app, Computable.fin_app
list 📖	CompOp	34 math math: Primrec.vector_toList_iff, Computable.list_getElem?, Computable.list_reverse, Computable.list_cons, Primrec.list_length, Computable.list_concat, Primrec.listFilter, Primrec.list_idxOf, PrimrecRel.listFilter, Primrec.list_concat, PrimrecRel.exists_mem_list, Primrec.list_range, Primrec.list_headI, Computable.list_length, Primrec.list_cons, Primrec.vector_toList, Computable.list_append, Computable.vector_toList, Primrec.list_flatten, Primrec.list_tail, PrimrecPred.exists_mem_list, Primrec.list_getElem?, Primrec.list_getD, Primrec.optionToList, Computable.list_ofFn, PrimrecPred.forall_mem_list, Primrec.list_reverse, Primrec.list_getI, PrimrecRel.forall_mem_list, Primrec.list_ofFn, PrimrecPred.listFilter_listRange, Primrec.list_head?, Primrec.list_append, Primrec.listLookup
vector 📖	CompOp	25 math math: Computable.vector_cons, Primrec.vector_toList_iff, Nat.Partrec'.to_part, Primrec.vector_ofFn', Partrec.vector_mOfFn, Nat.Primrec'.prim_iff, Primrec.vector_tail, Computable.vector_ofFn', Primrec.vector_get, Computable.vector_ofFn, Computable.vector_head, Nat.Partrec'.part_iff, Primrec.vector_toList, Nat.Partrec'.vec_iff, Primrec.vector_cons, Nat.Primrec'.to_prim, Computable.vector_toList, Computable.vector_length, Primrec.vector_ofFn, Primrec.vector_length, Nat.Primrec'.vec_iff, Primrec.vector_get', Computable.vector_get, Computable.vector_tail, Primrec.vector_head

Primrec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fin_app 📖	mathematical	—	Primrec₂ Primcodable.finArrow Primcodable.fin	—	of_eq Primrec₂.comp vector_get comp vector_ofFn' fst snd List.Vector.get_ofFn
fin_curry 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.finArrow Encodable.decode Primrec₂ Primcodable.fin	—	Primrec₂.comp fin_app comp fst snd of_eq vector_get' vector_ofFn id const List.Vector.get_ofFn
fin_curry₁ 📖	mathematical	—	Primrec₂ Primcodable.fin Encodable.encode Option.encodable Primcodable.toEncodable Encodable.decode	—	Primrec₂.comp const id of_eq vector_get comp vector_ofFn snd fst List.Vector.get_ofFn
listFilter 📖	mathematical	PrimrecPred	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	listFilterMap id ite PrimrecPred.comp snd option_some_iff const
listFilterMap 📖	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂ Primcodable.option	—	—	of_eq list_flatMap comp₂ optionToList List.filterMap_eq_flatMap_toList
listLookup 📖	mathematical	—	Primrec₂ Primcodable.list Primcodable.prod Primcodable.option	—	Primrec₂.of_eq to₂ snd const cond Primrec₂.comp beq comp fst option_some
list_append 📖	mathematical	—	Primrec₂ Primcodable.list	—	Primrec₂.of_eq to₂ list_foldr fst snd comp list_cons
list_casesOn 📖	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂ Primcodable.prod	—	—	Primcodable.prim
list_concat 📖	mathematical	—	Primrec₂ Primcodable.list	—	Primrec₂.comp list_append fst list_cons snd const
list_cons 📖	mathematical	—	Primrec₂ Primcodable.list	—	Primcodable.prim
list_findIdx 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂ Primcodable.bool	Primcodable.ofDenumerable Denumerable.nat	—	of_eq list_foldr const to₂ cond Primrec₂.comp fst comp snd succ
list_flatMap 📖	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂	—	—	comp list_flatten list_map
list_flatten 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	of_eq list_foldr id const to₂ comp list_append snd
list_foldl 📖	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂ Primcodable.prod	—	—	Primcodable.prim
list_foldr 📖	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂ Primcodable.prod	—	—	of_eq list_foldl comp list_reverse to₂ Primrec₂.comp fst pair snd
list_getD 📖	mathematical	—	Primrec₂ Primcodable.list Primcodable.ofDenumerable Denumerable.nat	—	Primrec₂.comp₂ option_getD list_getElem? const
list_getElem? 📖	mathematical	—	Primrec₂ Primcodable.list Primcodable.ofDenumerable Denumerable.nat Primcodable.option	—	to₂ list_foldl fst comp sumInl snd sumCasesOn sumInr const option_some Primrec₂.of_eq zero_add Nat.instZeroLEOneClass IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd
list_getI 📖	mathematical	—	Primrec₂ Primcodable.list Primcodable.ofDenumerable Denumerable.nat List.getI	—	list_getD
list_head? 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.option Encodable.decode Primcodable.list	—	of_eq id const to₂ option_some_iff comp fst snd
list_headI 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable List.headI Encodable.decode Primcodable.list	—	of_eq comp option_getD_default list_head? List.head!_eq_head?_getD
list_idxOf 📖	mathematical	—	Primrec₂ Primcodable.list Primcodable.ofDenumerable Denumerable.nat	—	to₂ list_findIdx snd Primrec₂.comp₂ beq comp fst
list_length 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable Denumerable.nat Encodable.decode Primcodable.list	—	of_eq list_foldr id const to₂ comp succ snd
list_map 📖	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂	—	—	of_eq list_foldr const to₂ Primrec₂.comp list_cons fst comp snd
list_ofFn 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Encodable.decode	Primcodable.list	—	const Primrec₂.comp list_cons
list_range 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Primcodable.ofDenumerable Denumerable.nat Encodable.decode	—	of_eq nat_rec' id const to₂ comp Primrec₂.comp list_concat snd fst
list_rec 📖	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂ Primcodable.prod	—	—	list_foldr pair const to₂ comp Primrec₂.comp list_cons fst snd of_eq
list_reverse 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	Primcodable.prim
list_tail 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	of_eq id const to₂ comp snd
nat_omega_rec 📖	—	Primrec₂ Primcodable.ofDenumerable Denumerable.nat Primcodable.list Primcodable.prod Primcodable.option	—	—	Primrec₂.uncurry nat_omega_rec' list_map Primrec₂.comp fst snd Primrec₂.comp₂ Primrec₂.pair comp₂ Primrec₂.left Primrec₂.right
nat_omega_rec' 📖	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable Denumerable.nat Encodable.decode Primcodable.list Primrec₂ Primcodable.option	—	—	to₂ list_flatMap snd comp₂ optionToList Primrec₂.comp₂ listLookup Primrec₂.right fst Primrec₂.left nat_rec' Primrec₂.comp list_cons const comp listFilterMap nat_sub option_map Primrec₂.pair list_getElem? id succ option_some_iff of_eq tsub_zero Nat.instOrderedSub IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass Nat.instCanonicallyOrderedAdd List.lookup_graph List.filterMap_eq_map_iff_forall_eq_some List.infix_flatMap_of_mem zero_add
nat_sqrt 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable Denumerable.nat Encodable.decode	—	Nat.Primrec'.prim_iff₁ Nat.Primrec'.sqrt
nat_strong_rec 📖	mathematical	Primrec₂ Primcodable.list Primcodable.option	Primcodable.ofDenumerable Denumerable.nat	—	Primrec₂.option_some_iff Primrec₂.of_eq const to₂ option_bind comp snd option_map Primrec₂.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
optionToList 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primcodable.option	—	of_eq id const comp₂ Primrec₂.comp list_cons Primrec₂.right
vector_cons 📖	mathematical	—	Primrec₂ List.Vector Primcodable.vector List.Vector.cons	—	vector_toList_iff List.Vector.toList_cons Primrec₂.comp list_cons fst snd
vector_get 📖	mathematical	—	Primrec₂ List.Vector Primcodable.vector Primcodable.fin List.Vector.get	—	option_some_iff of_eq Primrec₂.comp list_getElem? comp vector_toList fst fin_val snd List.Vector.toList_length
vector_get' 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.finArrow List.Vector List.Vector.get Encodable.decode Primcodable.vector	—	of_equiv_symm
vector_head 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable List.Vector List.Vector.head Encodable.decode Primcodable.vector	—	option_some_iff of_eq comp list_head? vector_toList
vector_length 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable Denumerable.nat List.Vector List.Vector.length Encodable.decode Primcodable.vector	—	const
vector_ofFn 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Encodable.decode	List.Vector Primcodable.vector List.Vector.ofFn	—	vector_toList_iff List.Vector.toList_ofFn list_ofFn
vector_ofFn' 📖	mathematical	—	Encodable.encode List.Vector Option.encodable Primcodable.toEncodable Primcodable.vector List.Vector.ofFn Encodable.decode Primcodable.finArrow	—	of_equiv
vector_tail 📖	mathematical	—	Encodable.encode List.Vector Option.encodable Primcodable.toEncodable Primcodable.vector List.Vector.tail Encodable.decode	—	vector_toList_iff of_eq comp list_tail vector_toList
vector_toList 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list List.Vector List.Vector.toList Encodable.decode Primcodable.vector	—	subtype_val
vector_toList_iff 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list List.Vector.toList Encodable.decode List.Vector Primcodable.vector	—	subtype_val_iff

PrimrecPred

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lt 📖	—	PrimrecPred Primcodable.ofDenumerable Denumerable.nat	—	—	of_eq comp exists_mem_list Primrec.list_range
exists_mem_list 📖	mathematical	PrimrecPred	Primcodable.list	—	of_eq not PrimrecRel.comp Primrec.eq Primrec.comp Primrec.list_length Primrec.listFilter Primrec.primrecPred Primrec.const
forall_lt 📖	—	PrimrecPred Primcodable.ofDenumerable Denumerable.nat	—	—	of_eq comp forall_mem_list Primrec.list_range
forall_mem_list 📖	mathematical	PrimrecPred	Primcodable.list	—	of_eq PrimrecRel.comp Primrec.eq Primrec.comp Primrec.list_length Primrec.listFilter Primrec.primrecPred
listFilter_listRange 📖	mathematical	PrimrecRel Primcodable.ofDenumerable Denumerable.nat	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	Primrec.listFilterMap Primrec.const Primrec.ite PrimrecRel.comp Primrec.eq Primrec₂.comp PrimrecRel.decide Primrec.snd Primrec.fst Primrec.option_some_iff

PrimrecRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lt 📖	—	PrimrecRel Primcodable.ofDenumerable Denumerable.nat	—	—	PrimrecPred.of_eq comp exists_mem_list Primrec.comp Primrec.list_range Primrec.fst Primrec.snd
exists_mem_list 📖	mathematical	PrimrecRel	Primcodable.list	—	of_eq not comp Primrec.eq Primrec.comp Primrec.list_length listFilter Primrec.const
forall_lt 📖	—	PrimrecRel Primcodable.ofDenumerable Denumerable.nat	—	—	PrimrecPred.of_eq comp forall_mem_list Primrec.comp Primrec.list_range Primrec.fst Primrec.snd
forall_mem_list 📖	mathematical	PrimrecRel	Primcodable.list	—	of_eq comp Primrec.eq Primrec.comp Primrec.list_length listFilter Primrec.fst
listFilter 📖	mathematical	PrimrecRel	Primrec₂ Primcodable.list	—	Primrec.listFilterMap Primrec.fst Primrec.ite comp Primrec.eq Primrec₂.comp decide Primrec.snd Primrec.comp Primrec.const Primrec.option_some

---

← Back to Index