Documentation Verification Report

Basic

📁 Source: Mathlib/Data/Seq/Basic.lean

Statistics

MetricCount
DefinitionsinstFunctor, bind, coeSeq, instInhabited, join, map, monad, ret, toSeq
9
Theoremscoind, coind_trans, cons, cons_cons_of_trans, cons_elim, nil, Pairwise_cons_cons_head, Pairwise_cons_nil, Pairwise_drop, Pairwise_tail, all_coind, all_coind_drop_motive, all_cons, all_get, all_of_get, append_assoc, append_nil, at_least_as_long_as_coind, cons_append, drop_get?, drop_length', drop_nil, drop_set_of_lt, drop_succ_cons, drop_zero, dropn_add, dropn_tail, enum_cons, enum_nil, exists_of_mem_map, fold_cons, fold_head, fold_nil, get?_enum, get?_mem_take, get?_set_of_ne, get?_set_of_not_terminatedAt, get?_set_of_terminatedAt, get?_update, get?_zip, get?_zipWith, getElem?_take, getElem?_toList, getLast?_toList, head_dropn, instLawfulFunctor, join_append, join_cons, join_cons_cons, join_cons_nil, join_nil, length'_cons, length'_eq_zero_iff_nil, length'_le_iff, length'_map, length'_ne_zero_iff_cons, length'_nil, length'_of_not_terminates, length'_of_terminates, length_cons, length_eq_zero, length_le_iff, length_le_iff', length_map, length_nil, length_take_le, length_take_of_le_length, length_toList, lt_length'_iff, lt_length_iff, lt_length_iff', map_all_iff, map_append, map_comp, map_cons, map_get?, map_id, map_nil, map_tail, mem_append_left, mem_map, nats_get?, nil_append, ofList_append, ofList_toList, ofStream_append, ofStream_cons, of_mem_append, set_all, set_cons_succ, set_cons_zero, set_nil, take_all, take_drop, take_nil, take_succ_cons, take_zero, terminatedAt_map_iff, terminatedAt_ofList, terminates_map_iff, terminates_ofList, toList_nil, toList_ofList, update_cons_succ, update_cons_zero, update_nil, zipWith_cons_cons, zipWith_map, zipWith_map_left, zipWith_map_right, zipWith_nil_left, zipWith_nil_right, zip_cons_cons, zip_map, zip_map_left, zip_map_right, zip_nil_left, zip_nil_right, bind_assoc, bind_ret, join_cons, join_join, join_map_ret, join_nil, lawfulMonad, map_id, map_join, map_join', map_pair, ret_bind
130
Total139

Stream'.Seq

Definitions

NameCategoryTheorems
instFunctor 📖CompOp
1 mathmath: instLawfulFunctor

Theorems

NameKindAssumesProvesValidatesDepends On
Pairwise_cons_cons_head 📖Pairwise
cons
Pairwise_cons_nil 📖mathematicalPairwise
cons
nil
Pairwise.cons
instIsEmptyFalse
Pairwise_drop 📖mathematicalPairwisedropPairwise_tail
Pairwise_tail 📖mathematicalPairwisetailPairwise.cons_elim
all_coind 📖Stream'.Seq
instMembership
all_of_get
all_coind_drop_motive
head_dropn
instIsEmptyFalse
head_cons
all_coind_drop_motive 📖mathematicaldrop
all_cons 📖Stream'.Seq
instMembership
cons
all_get 📖get?get?_mem
all_of_get 📖Stream'.Seq
instMembership
append_assoc 📖mathematicalappendeq_of_bisim
nil_append
destruct_cons
append_nil
cons_append
append_nil 📖mathematicalappend
nil
coinduction2
cons_append
destruct_cons
at_least_as_long_as_coind 📖mathematicalconsENat
Preorder.toLE
PartialOrder.toPreorder
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
instLinearOrderENat
length'
length'_of_terminates
drop_length'
top_add
tsub_self
length'_cons
length'_of_not_terminates
cons_append 📖mathematicalappend
cons
destruct_eq_cons
corec_eq
destruct_cons
drop_get? 📖mathematicalget?
drop
zero_add
drop_length' 📖mathematicallength'
drop
ENat
instSubENat
ENat.instNatCast
drop_nil 📖mathematicaldrop
nil
drop_set_of_lt 📖mathematicaldrop
set
ext
drop_get?
get?_set_of_ne
drop_succ_cons 📖mathematicaldrop
cons
drop_zero 📖mathematicaldrop
dropn_add 📖mathematicaldrop
dropn_tail 📖mathematicaldrop
tail
dropn_add
enum_cons 📖mathematicalenum
cons
map
ext
get?_enum
map_get?
enum_nil 📖mathematicalenum
nil
exists_of_mem_map 📖Stream'.Seq
instMembership
map
Stream'.exists_of_mem_map
fold_cons 📖mathematicalfold
cons
corec_cons
destruct_cons
fold_head 📖mathematicalhead
fold
head_cons
fold_nil 📖mathematicalfold
nil
cons
corec_nil
get?_enum 📖mathematicalget?
enum
get?_zip
get?_mem_take 📖mathematicalget?taketake.eq_2
head_eq_some
destruct_cons
ge_stable
covariant_swap_add_of_covariant_add
IsOrderedAddMonoid.toAddLeftMono
Nat.instIsOrderedAddMonoid
IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT
AddRightCancelSemigroup.toIsRightCancelAdd
contravariant_swap_add_of_contravariant_add
contravariant_lt_of_covariant_le
Nat.instCanonicallyOrderedAdd
get?_tail
get?_set_of_ne 📖mathematicalget?
set
get?_update
get?_set_of_not_terminatedAt 📖mathematicalTerminatedAtget?
set
Function.update_self
get?_set_of_terminatedAt 📖mathematicalTerminatedAtget?
set
get?_update
get?_update 📖mathematicalget?
update
get?_zip 📖mathematicalget?
zip
Option.map₂
get?_zipWith
get?_zipWith 📖mathematicalget?
zipWith
Option.map₂
getElem?_take 📖mathematicaltake
get?
Nat.instCanonicallyOrderedAdd
take.eq_2
Nat.instNoMaxOrder
destruct_eq_none
destruct_eq_cons
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
getElem?_toList 📖mathematicalTerminatestoList
get?
getElem?_take
ge_stable
getLast?_toList 📖mathematicalTerminatestoList
get?
length
getElem?_toList
length_toList
head_dropn 📖mathematicalhead
drop
get?
get?_tail
dropn_tail
instLawfulFunctor 📖mathematicalStream'.Seq
instFunctor
map_id
map_comp
join_append 📖mathematicaljoin
append
Stream'.Seq1
eq_of_bisim
nil_append
join_nil
join_cons
destruct_cons
cons_append
append_assoc
join_cons 📖mathematicaljoin
cons
Stream'.Seq1
Stream'.Seq
append
eq_of_bisim
destruct_cons
join_cons_nil
nil_append
join_cons_cons
cons_append
join_cons_cons 📖mathematicaljoin
cons
Stream'.Seq1
Stream'.Seq
destruct_eq_cons
corec_eq
destruct_cons
join_cons_nil 📖mathematicaljoin
cons
Stream'.Seq1
Stream'.Seq
nil
destruct_eq_cons
corec_eq
destruct_cons
join_nil 📖mathematicaljoin
nil
Stream'.Seq1
destruct_eq_none
length'_cons 📖mathematicallength'
cons
ENat
Distrib.toAdd
NonUnitalNonAssocSemiring.toDistrib
NonAssocSemiring.toNonUnitalNonAssocSemiring
Semiring.toNonAssocSemiring
CommSemiring.toSemiring
instCommSemiringENat
AddMonoidWithOne.toOne
AddCommMonoidWithOne.toAddMonoidWithOne
NonAssocSemiring.toAddCommMonoidWithOne
terminates_cons_iff
length'_of_terminates
length_cons
Nat.cast_add
Nat.cast_one
length'_of_not_terminates
top_add
length'_eq_zero_iff_nil 📖mathematicallength'
ENat
instZeroENat
nil
length'_nil
length'_cons
Unique.instSubsingleton
NeZero.one
length'_le_iff 📖mathematicalENat
Preorder.toLE
PartialOrder.toPreorder
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
instLinearOrderENat
length'
ENat.instNatCast
TerminatedAt
length'_of_terminates
IsOrderedAddMonoid.toAddLeftMono
IsOrderedRing.toIsOrderedAddMonoid
IsOrderedRing.toZeroLEOneClass
length_le_iff
length'_of_not_terminates
length'_map 📖mathematicallength'
map
length'_of_terminates
terminates_map_iff
length_map
length'_of_not_terminates
length'_ne_zero_iff_cons 📖mathematicalconslength'_nil
length'_cons
Unique.instSubsingleton
NeZero.one
length'_nil 📖mathematicallength'
nil
ENat
instZeroENat
length_nil
Nat.cast_zero
length'_of_not_terminates 📖mathematicalTerminateslength'
Top.top
ENat
instTopENat
length'_of_terminates 📖mathematicalTerminateslength'
ENat
ENat.instNatCast
length
length_cons 📖mathematicalTerminateslength
cons
terminates_cons_iff
Nat.find_comp_succ
terminates_cons_iff
length_eq_zero 📖mathematicalTerminateslength
nil
length_le_iff 📖mathematicalTerminateslength
TerminatedAt
length_le_iff'
length_le_iff' 📖mathematicallength
TerminatedAt
le_stable
le_rfl
length_map 📖mathematicalTerminates
map
length
terminates_map_iff
terminates_map_iff
length.eq_1
length_nil 📖mathematicallength
nil
terminates_nil
terminates_nil
length_take_le 📖mathematicaltaketake_zero
take.eq_2
covariant_swap_add_of_covariant_add
IsOrderedAddMonoid.toAddLeftMono
Nat.instIsOrderedAddMonoid
IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT
AddRightCancelSemigroup.toIsRightCancelAdd
contravariant_swap_add_of_contravariant_add
contravariant_lt_of_covariant_le
Nat.instCanonicallyOrderedAdd
length_take_of_le_length 📖mathematicallengthtaketake.eq_2
destruct.eq_1
lt_length_iff'
lt_of_lt_of_le
le_stable
length_toList 📖mathematicalTerminatestoList
length
toList.eq_1
length_take_of_le_length
le_rfl
lt_length'_iff 📖mathematicalENat
Preorder.toLT
PartialOrder.toPreorder
SemilatticeInf.toPartialOrder
Lattice.toSemilatticeInf
DistribLattice.toLattice
instDistribLatticeOfLinearOrder
instLinearOrderENat
ENat.instNatCast
length'
get?
length'_of_terminates
IsOrderedAddMonoid.toAddLeftMono
IsOrderedRing.toIsOrderedAddMonoid
IsOrderedRing.toZeroLEOneClass
lt_length_iff
length'_of_not_terminates
not_terminates_iff
lt_length_iff 📖mathematicalTerminateslength
get?
lt_length_iff'
lt_length_iff' 📖mathematicallength
get?
le_rfl
le_stable
map_all_iff 📖mem_map
exists_of_mem_map
map_append 📖mathematicalmap
append
eq_of_bisim
nil_append
map_cons
destruct_cons
cons_append
map_comp 📖mathematicalmap
map_cons 📖mathematicalmap
cons
Stream'.map_cons
map_get? 📖mathematicalget?
map
map_id 📖mathematicalmapStream'.map_id
map_nil 📖mathematicalmap
nil
map_tail 📖mathematicalmap
tail
mem_append_left 📖mathematicalStream'.Seq
instMembership
appendmem_rec_on
cons_append
mem_map 📖mathematicalStream'.Seq
instMembership
mapStream'.mem_map
nats_get? 📖mathematicalget?
nats
nil_append 📖mathematicalappend
nil
coinduction2
corec_eq
destruct_cons
ofList_append 📖mathematicalofList
append
nil_append
ofList_cons
cons_append
ofList_toList 📖mathematicalTerminatesofList
toList
ext
getElem?_toList
ofStream_append 📖mathematicalofStream
Stream'.appendStream'
append
ofList
nil_append
ofStream_cons
ofList_cons
cons_append
ofStream_cons 📖mathematicalofStream
Stream'.cons
cons
Stream'.map_cons
of_mem_append 📖Stream'.Seq
instMembership
append
mem_rec_on
nil_append
cons_append
mem_cons
destruct_cons
mem_cons_of_mem
set_all 📖Stream'.Seq
instMembership
set
eq_or_ne
get?_set_of_terminatedAt
get?_set_of_not_terminatedAt
get?_mem
get?_set_of_ne
set_cons_succ 📖mathematicalset
cons
update_cons_succ
set_cons_zero 📖mathematicalset
cons
update_cons_zero
set_nil 📖mathematicalset
nil
update_nil
take_all 📖taketake_nil
take_succ_cons
take_drop 📖mathematicaltake
drop
take_nil 📖mathematicaltake
nil
take_succ_cons 📖mathematicaltake
cons
take_zero 📖mathematicaltake
terminatedAt_map_iff 📖mathematicalTerminatedAt
map
map_get?
terminatedAt_ofList 📖mathematicalTerminatedAt
ofList
terminates_map_iff 📖mathematicalTerminates
map
terminates_ofList 📖mathematicalTerminates
ofList
terminatedAt_ofList
toList_nil 📖mathematicaltoList
nil
TerminatedAt
Stream'.Seq
terminatedAt_zero_iff
terminatedAt_zero_iff
getElem?_take
Nat.instCanonicallyOrderedAdd
toList_ofList 📖mathematicaltoList
ofList
terminates_ofList
ofList_injective
terminates_ofList
ofList_toList
update_cons_succ 📖mathematicalupdate
cons
ext
get?_update
update_cons_zero 📖mathematicalupdate
cons
ext
get?_update
update_nil 📖mathematicalupdate
nil
ext
get?_update
zipWith_cons_cons 📖mathematicalzipWith
cons
ext
Option.map₂_coe_right
zipWith_map 📖mathematicalzipWith
map
ext
map_get?
Option.map₂_none_right
Option.map₂_coe_right
zipWith_map_left 📖mathematicalzipWith
map
map_id
zipWith_map
zipWith_map_right 📖mathematicalzipWith
map
map_id
zipWith_map
zipWith_nil_left 📖mathematicalzipWith
nil
zipWith_nil_right 📖mathematicalzipWith
nil
ext
Option.map₂_none_right
zip_cons_cons 📖mathematicalzip
cons
zipWith_cons_cons
zip_map 📖mathematicalzip
map
ext
get?_zip
map_get?
Option.map₂_none_right
Option.map₂_coe_right
zip_map_left 📖mathematicalzip
map
map_id
zip_map
zip_map_right 📖mathematicalzip
map
map_id
zip_map
zip_nil_left 📖mathematicalzip
nil
zip_nil_right 📖mathematicalzip
nil
zipWith_nil_right

Stream'.Seq.Pairwise

Theorems

NameKindAssumesProvesValidatesDepends On
coind 📖mathematicalStream'.Seq.PairwiseStream'.Seq.all_coind_drop_motive
Stream'.Seq.head_dropn
Stream'.Seq.dropn_add
Stream'.Seq.all_get
Stream'.Seq.head_cons
coind_trans 📖mathematicalStream'.Seq.PairwiseStream'.Seq.all_coind_drop_motive
Stream'.Seq.head_eq_some
Stream'.Seq.head_dropn
Stream'.Seq.ge_stable
trans
cons 📖mathematicalStream'.Seq.PairwiseStream'.Seq.consNat.instCanonicallyOrderedAdd
Stream'.Seq.all_get
cons_cons_of_trans 📖Stream'.Seq.Pairwise
Stream'.Seq.cons
cons
cons_elim
cons_elim 📖Stream'.Seq.Pairwise
Stream'.Seq.cons
Stream'.Seq.mem_iff_exists_get?
nil 📖mathematicalStream'.Seq.Pairwise
Stream'.Seq.nil
instIsEmptyFalse

Stream'.Seq1

Definitions

NameCategoryTheorems
bind 📖CompOp
3 mathmath: ret_bind, bind_assoc, bind_ret
coeSeq 📖CompOp
instInhabited 📖CompOp
join 📖CompOp
4 mathmath: map_join, join_cons, join_join, join_nil
map 📖CompOp
5 mathmath: map_id, bind_ret, map_join, map_pair, map_join'
monad 📖CompOp
1 mathmath: lawfulMonad
ret 📖CompOp
3 mathmath: ret_bind, join_map_ret, bind_ret
toSeq 📖CompOp

Theorems

NameKindAssumesProvesValidatesDepends On
bind_assoc 📖mathematicalbindmap_join
Stream'.Seq.map_comp
join_join
Stream'.Seq.join_nil
join_cons
Stream'.Seq.join_cons
Stream'.Seq.join_append
Stream'.Seq.nil_append
Stream'.Seq.cons_append
Stream'.Seq.append_assoc
Stream'.Seq.append_nil
bind_ret 📖mathematicalbind
Stream'.Seq1
ret
map
Stream'.Seq.map_comp
join_map_ret
join_cons 📖mathematicaljoin
Stream'.Seq1
Stream'.Seq
Stream'.Seq.cons
Stream'.Seq.join
Stream'.Seq.destruct_cons
join_join 📖mathematicalStream'.Seq.join
Stream'.Seq1
Stream'.Seq.map
join
Stream'.Seq.eq_of_bisim
Stream'.Seq.nil_append
Stream'.Seq.join_nil
Stream'.Seq.map_cons
Stream'.Seq.join_cons
Stream'.Seq.join_append
Stream'.Seq.destruct_cons
Stream'.Seq.cons_append
join_cons
Stream'.Seq.append_assoc
join_map_ret 📖mathematicalStream'.Seq.join
Stream'.Seq.map
Stream'.Seq1
ret
Stream'.Seq.coinduction2
Stream'.Seq.join_nil
Stream'.Seq.map_cons
Stream'.Seq.join_cons
Stream'.Seq.nil_append
Stream'.Seq.destruct_cons
join_nil 📖mathematicaljoin
Stream'.Seq1
Stream'.Seq
Stream'.Seq.nil
Stream'.Seq.join
lawfulMonad 📖mathematicalStream'.Seq1
monad
map_id
ret_bind
bind_assoc
bind_ret
map_id 📖mathematicalmapStream'.Seq.map_id
map_join 📖mathematicalmap
join
Stream'.Seq1
map_join'
join_cons
Stream'.Seq.join_cons
Stream'.Seq.map_cons
Stream'.Seq.map_append
map_join' 📖mathematicalStream'.Seq.map
Stream'.Seq.join
Stream'.Seq1
map
Stream'.Seq.eq_of_bisim
Stream'.Seq.nil_append
Stream'.Seq.join_nil
Stream'.Seq.map_cons
Stream'.Seq.join_cons
Stream'.Seq.map_append
Stream'.Seq.destruct_cons
Stream'.Seq.cons_append
map_pair 📖mathematicalmap
Stream'.Seq
Stream'.Seq.map
ret_bind 📖mathematicalbind
ret
Stream'.Seq.join_nil
join_cons
Stream'.Seq.join_cons
Stream'.Seq.append_nil

---

← Back to Index