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_drop, list_dropWhile, 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_modify, list_modify', list_modifyHead, list_modifyHead', list_ofFn, list_range, list_rec, list_reverse, list_set, list_tail, list_take, list_takeWhile, 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	88
Total	92

Nat

Definitions

Name	Category	Theorems
Primrec' 📖	CompData	22 math math: Primrec'.sub, Primrec'.comp₁, Primrec'.unpair₁, Primrec'.encode, Primrec'.natPair, Primrec'.pred, Primrec'.if_lt, Primrec'.head, Primrec'.prec', Primrec'.prim_iff₂, Primrec'.prim_iff, Primrec'.comp', Primrec'.unpair₂, Primrec'.add, Primrec'.of_prim, Primrec'.prim_iff₁, Primrec'.comp₂, Primrec'.tail, Primrec'.of_eq, 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' 📖	mathematical	Nat.Primrec' Vec	Nat.Primrec'	—	of_eq List.Vector.ofFn_get
comp₁ 📖	mathematical	Nat.Primrec' List.Vector.head	Nat.Primrec'	—	—
comp₂ 📖	mathematical	Nat.Primrec' List.Vector.head List.Vector.tail	Nat.Primrec'	—	List.Vector.head_cons List.Vector.tail_cons comp' cons nil
cons 📖	mathematical	Nat.Primrec' Vec	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 📖	mathematical	Nat.Primrec'	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 📖	mathematical	Nat.Primrec'	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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
prec' 📖	mathematical	Nat.Primrec'	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'	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.Primrec' Nat.unpair	—	comp₁ sqrt comp₂ sub mul of_eq if_lt
unpair₂ 📖	mathematical	Nat.Primrec'	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	46 math math: Primrec.vector_toList_iff, Computable.list_getElem?, Computable.list_reverse, Computable.list_cons, Primrec.list_set, Primrec.list_length, Computable.list_concat, Primrec.listFilter, Primrec.list_idxOf, PrimrecRel.listFilter, Primrec.list_modify', Primrec.list_concat, PrimrecRel.exists_mem_list, Primrec.list_modifyHead, Primrec.list_range, Primrec.list_headI, Primrec.list_map, Computable.list_length, Primrec.list_drop, Primrec.list_cons, Primrec.list_modifyHead', Primrec.vector_toList, Computable.list_append, Computable.vector_toList, Primrec.list_flatten, Primrec.list_tail, PrimrecPred.exists_mem_list, Primrec.list_getElem?, Primrec.list_dropWhile, Primrec.list_flatMap, Primrec.list_getD, Primrec.optionToList, Computable.list_ofFn, Primrec.list_take, PrimrecPred.forall_mem_list, Primrec.list_modify, Primrec.list_reverse, Primrec.list_getI, PrimrecRel.forall_mem_list, Primrec.list_ofFn, PrimrecPred.listFilter_listRange, Primrec.list_head?, Primrec.list_takeWhile, Primrec.list_append, Primrec.listFilterMap, 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 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂ Primcodable.option	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	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 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂ Primcodable.prod	Encodable.encode Option.encodable Primcodable.toEncodable Encodable.decode	—	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_drop 📖	mathematical	—	Primrec₂ Primcodable.ofDenumerable Denumerable.nat Primcodable.list	—	Primrec₂.of_eq to₂ nat_iterate fst snd comp₂ list_tail Primrec₂.right List.tail_iterate
list_dropWhile 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.bool Encodable.decode	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	of_eq Primrec₂.comp list_drop list_findIdx id to₂ comp not snd
list_findIdx 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂ Primcodable.bool	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable Denumerable.nat Encodable.decode	—	of_eq list_foldr const to₂ cond Primrec₂.comp fst comp snd succ
list_flatMap 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	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 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂ Primcodable.prod	Encodable.encode Option.encodable Primcodable.toEncodable Encodable.decode	—	Primcodable.prim
list_foldr 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂ Primcodable.prod	Encodable.encode Option.encodable Primcodable.toEncodable Encodable.decode	—	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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add 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 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	of_eq list_foldr const to₂ Primrec₂.comp list_cons fst comp snd
list_modify 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Encodable.decode	Primrec₂ Primcodable.list Primcodable.ofDenumerable Denumerable.nat	—	to₂ Primrec₂.comp list_modify' comp snd fst pair const
list_modify' 📖	mathematical	Primrec₂	Primrec₂ Primcodable.list Primcodable.prod Primcodable.ofDenumerable Denumerable.nat	—	Primrec₂.of_eq to₂ Primrec₂.comp list_append list_take comp fst snd list_modifyHead' list_drop
list_modifyHead 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Encodable.decode	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	Primrec₂.comp list_modifyHead' to₂ comp snd id const
list_modifyHead' 📖	mathematical	Primrec₂	Primrec₂ Primcodable.list	—	Primrec₂.of_eq to₂ fst const Primrec₂.comp list_cons comp snd
list_ofFn 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Encodable.decode	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	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 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode Primrec₂ Primcodable.prod	Encodable.encode Option.encodable Primcodable.toEncodable Encodable.decode	—	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_set 📖	mathematical	—	Primrec₂ Primcodable.list Primcodable.prod Primcodable.ofDenumerable Denumerable.nat	—	Primrec₂.of_eq list_modify' to₂ fst
list_tail 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	of_eq id const to₂ comp snd
list_take 📖	mathematical	—	Primrec₂ Primcodable.ofDenumerable Denumerable.nat Primcodable.list	—	of_eq comp list_reverse Primrec₂.comp list_drop nat_sub list_length snd fst
list_takeWhile 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.bool Encodable.decode	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.list Encodable.decode	—	of_eq Primrec₂.comp list_take list_findIdx id to₂ comp not snd
nat_omega_rec 📖	mathematical	Primrec₂ Primcodable.ofDenumerable Denumerable.nat Primcodable.list Primcodable.prod Primcodable.option	Primrec₂	—	Primrec₂.uncurry nat_omega_rec' list_map Primrec₂.comp fst snd Primrec₂.comp₂ Primrec₂.pair comp₂ Primrec₂.left Primrec₂.right
nat_omega_rec' 📖	mathematical	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable Denumerable.nat Encodable.decode Primcodable.list Primrec₂ Primcodable.option	Encodable.encode Option.encodable Primcodable.toEncodable Encodable.decode	—	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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass Nat.instCanonicallyOrderedAdd List.lookup_graph List.filterMap_congr 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	Primrec₂ 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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	Encodable.encode List.Vector Option.encodable Primcodable.toEncodable Primcodable.vector List.Vector.ofFn Encodable.decode	—	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 📖	mathematical	PrimrecPred Primcodable.ofDenumerable Denumerable.nat	PrimrecPred Primcodable.ofDenumerable Denumerable.nat	—	of_eq comp exists_mem_list Primrec.list_range
exists_mem_list 📖	mathematical	PrimrecPred	PrimrecPred Primcodable.list	—	of_eq not PrimrecRel.comp Primrec.eq Primrec.comp Primrec.list_length Primrec.listFilter Primrec.primrecPred Primrec.const
forall_lt 📖	mathematical	PrimrecPred Primcodable.ofDenumerable Denumerable.nat	PrimrecPred Primcodable.ofDenumerable Denumerable.nat	—	of_eq comp forall_mem_list Primrec.list_range
forall_mem_list 📖	mathematical	PrimrecPred	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 Primcodable.ofDenumerable Denumerable.nat 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 📖	mathematical	PrimrecRel Primcodable.ofDenumerable Denumerable.nat	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	PrimrecRel Primcodable.list	—	of_eq not comp Primrec.eq Primrec.comp Primrec.list_length listFilter Primrec.const
forall_lt 📖	mathematical	PrimrecRel Primcodable.ofDenumerable Denumerable.nat	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	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