Stream

📁 Source: Batteries/Data/Stream.lean

Statistics

Metric	Count
Definitions Stream, Stream, Stream, drop, take, takeTR, loop	7
Theorems stream_drop_eq_drop, stream_take_eq_take_drop, fst_takeTR, fst_takeTR_loop, fst_take_succ, fst_take_zero, snd_takeTR, snd_takeTR_loop, snd_take_eq_drop, take_eq_takeTR	10
Total	17

Batteries.RBMap.Keys

Definitions

Name	Category	Theorems
Stream 📖	CompOp	—

Batteries.RBMap.Values

Definitions

Name	Category	Theorems
Stream 📖	CompOp	—

Batteries.RBNode

Definitions

Name	Category	Theorems
Stream 📖	CompData	5 math math: Stream.next?_toList, Batteries.RBMap.toStream_toList, Batteries.RBSet.toStream_eq, Batteries.RBMap.toStream_eq, Batteries.RBSet.toStream_toList

Std.List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stream_drop_eq_drop 📖	mathematical	—	Std.Stream.drop	—	—
stream_take_eq_take_drop 📖	mathematical	—	Std.Stream.take	—	—

Std.Stream

Definitions

Name	Category	Theorems
drop 📖	CompOp	4 math math: Std.List.stream_drop_eq_drop, snd_take_eq_drop, snd_takeTR, snd_takeTR_loop
take 📖	CompOp	7 math math: fst_takeTR_loop, fst_takeTR, fst_take_succ, snd_take_eq_drop, fst_take_zero, take_eq_takeTR, Std.List.stream_take_eq_take_drop
takeTR 📖	CompOp	3 math math: fst_takeTR, snd_takeTR, take_eq_takeTR

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fst_takeTR 📖	mathematical	—	takeTR take	—	fst_takeTR_loop
fst_takeTR_loop 📖	mathematical	—	takeTR.loop take	—	—
fst_take_succ 📖	mathematical	—	take	—	—
fst_take_zero 📖	mathematical	—	take	—	—
snd_takeTR 📖	mathematical	—	takeTR drop	—	snd_takeTR_loop
snd_takeTR_loop 📖	mathematical	—	takeTR.loop drop	—	—
snd_take_eq_drop 📖	mathematical	—	take drop	—	—
take_eq_takeTR 📖	mathematical	—	take takeTR	—	fst_takeTR snd_takeTR snd_take_eq_drop

Std.Stream.takeTR

Definitions

Name	Category	Theorems
loop 📖	CompOp	2 math math: Std.Stream.fst_takeTR_loop, Std.Stream.snd_takeTR_loop

---

← Back to Index