Defs

📁 Source: Mathlib/Data/WSeq/Defs.lean

Statistics

Metric	Count
Definitions all, any, collect, compute, filter, filterMap, find, findIndex, findIndexes, get, indexOf, indexesOf, inits, isEmpty, length, removeNth, scanl, splitAt, take, union, updateNth, zip, zipWith	23
Theorems out, length_eq_map, toList_terminates	3
Total	26

Stream'.WSeq

Definitions

Name	Category	Theorems
all 📖	CompOp	—
any 📖	CompOp	—
collect 📖	CompOp	—
compute 📖	CompOp	—
filter 📖	CompOp	—
filterMap 📖	CompOp	—
find 📖	CompOp	—
findIndex 📖	CompOp	—
findIndexes 📖	CompOp	—
get 📖	CompOp	—
indexOf 📖	CompOp	—
indexesOf 📖	CompOp	—
inits 📖	CompOp	—
isEmpty 📖	CompOp	—
length 📖	CompOp	1 math math: length_eq_map
removeNth 📖	CompOp	—
scanl 📖	CompOp	—
splitAt 📖	CompOp	—
take 📖	CompOp	—
union 📖	CompOp	—
updateNth 📖	CompOp	—
zip 📖	CompOp	—
zipWith 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
length_eq_map 📖	mathematical	—	length Computation.map toList	—	Computation.eq_of_bisim Computation.corec_eq Computation.destruct_map seq_destruct_cons seq_destruct_think
toList_terminates 📖	mathematical	—	Computation.Terminates toList	—	IsFinite.out

Stream'.WSeq.IsFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	Computation.Terminates Stream'.WSeq.toList	—	—

---

← Back to Index