Basic

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

Statistics

Metric	Count
Definitions WSeq, append, bind, coeList, coeSeq, coeStream, cons, destruct, aux, aux, drop, aux, flatten, get?, head, inhabited, join, map, membership, monad, nil, ofList, ofSeq, ofStream, recOn, ret, tail, aux, think, toList	30
Theorems append_assoc, append_nil, cons_append, destruct_append, destruct_cons, destruct_dropn, destruct_flatten, destruct_join, destruct_map, destruct_nil, destruct_ofSeq, destruct_some_of_destruct_tail_some, destruct_tail, destruct_terminates_of_get?_terminates, destruct_think, aux_none, dropn_add, dropn_cons, dropn_nil, dropn_ofSeq, dropn_tail, dropn_think, eq_or_mem_iff_mem, exists_dropn_of_mem, exists_get?_of_mem, exists_of_mem_bind, exists_of_mem_join, exists_of_mem_map, flatten_pure, flatten_think, get?_add, get?_mem, get?_ofSeq, get?_tail, get?_terminates_le, head_cons, head_nil, head_ofSeq, head_some_of_get?_some, head_some_of_head_tail_some, head_terminates_iff, head_terminates_of_get?_terminates, head_terminates_of_head_tail_terminates, head_terminates_of_mem, head_think, join_cons, join_nil, join_think, map_append, map_comp, map_cons, map_id, map_join, map_nil, map_ret, map_think, mem_append_left, mem_cons, mem_cons_iff, mem_cons_of_mem, mem_map, mem_of_mem_dropn, mem_of_mem_tail, mem_rec_on, mem_think, nil_append, notMem_nil, ofList_cons, ofList_nil, of_mem_append, seq_destruct_cons, seq_destruct_nil, seq_destruct_think, tail_cons, tail_nil, tail_ofSeq, tail_think, think_append, toList'_cons, toList'_map, toList'_nil, toList'_think, toList_cons, toList_nil, toList_ofList	85
Total	115

Stream'

Definitions

Name	Category	Theorems
WSeq 📖	CompOp	51 math math: WSeq.seq_destruct_cons, WSeq.head_terminates_iff, WSeq.seq_destruct_think, WSeq.get?_mem, WSeq.liftRel_destruct, WSeq.destruct_terminates_of_get?_terminates, WSeq.toList'_map, WSeq.destruct_ofSeq, Computation.exists_of_mem_parallel, WSeq.flatten_think, WSeq.map_join, WSeq.destruct_map, WSeq.join_ret, WSeq.toList'_nil, WSeq.bind_ret, WSeq.join_append, WSeq.Equiv.equivalence, WSeq.destruct_join, WSeq.toList'_cons, WSeq.LiftRel.equiv, WSeq.destruct_congr_iff, WSeq.bind_assoc_comp, WSeq.destruct_nil, WSeq.drop.aux_none, WSeq.join_join, WSeq.LiftRel.refl, WSeq.join_think, WSeq.liftRel_destruct_iff, WSeq.LiftRel.symm, WSeq.destruct_congr, WSeq.join_cons, WSeq.flatten_pure, WSeq.notMem_nil, WSeq.destruct_cons, WSeq.destruct_append, WSeq.mem_congr, WSeq.liftRel_dropn_destruct, WSeq.join_map_ret, WSeq.mem_cons_iff, Computation.terminates_parallel.aux, WSeq.destruct_tail, WSeq.mem_think, WSeq.toList'_think, WSeq.destruct_dropn, WSeq.destruct_think, WSeq.LiftRel.swap, WSeq.join_nil, WSeq.mem_cons, WSeq.LiftRelO.swap, WSeq.destruct_flatten, WSeq.LiftRel.trans

Stream'.WSeq

Definitions

Name	Category	Theorems
append 📖	CompOp	11 math math: join_append, append_assoc, liftRel_append, map_append, cons_append, join_cons, nil_append, append_nil, destruct_append, mem_append_left, think_append
bind 📖	CompOp	6 math math: bind_ret, bind_congr, bind_assoc_comp, liftRel_bind, ret_bind, bind_assoc
coeList 📖	CompOp	—
coeSeq 📖	CompOp	—
coeStream 📖	CompOp	—
cons 📖	CompOp	16 math math: dropn_cons, cons_congr, seq_destruct_cons, mem_cons_of_mem, map_cons, toList'_cons, liftRel_cons, ofList_cons, toList_cons, cons_append, join_cons, destruct_cons, mem_cons_iff, head_cons, tail_cons, mem_cons
destruct 📖	CompOp	18 math math: head_terminates_iff, liftRel_destruct, destruct_terminates_of_get?_terminates, destruct_ofSeq, destruct_map, destruct_join, destruct_congr_iff, destruct_nil, liftRel_destruct_iff, destruct_congr, destruct_cons, destruct_append, liftRel_dropn_destruct, exists_dropn_of_mem, destruct_tail, destruct_dropn, destruct_think, destruct_flatten
drop 📖	CompOp	12 math math: dropn_cons, productive_dropn, dropn_think, dropn_congr, dropn_ofSeq, get?_add, liftRel_dropn_destruct, exists_dropn_of_mem, dropn_add, dropn_tail, destruct_dropn, dropn_nil
flatten 📖	CompOp	6 math math: flatten_congr, flatten_think, flatten_pure, liftRel_flatten, flatten_equiv, destruct_flatten
get? 📖	CompOp	9 math math: productive_iff, exists_get?_of_mem, get?_tail, get?_congr, get?_add, get?_terminates_le, Productive.get?_terminates, get?_terminates, get?_ofSeq
head 📖	CompOp	11 math math: head_terminates_iff, head_congr, head_ofSeq, head_nil, head_some_of_get?_some, head_terminates, head_cons, head_terminates_of_head_tail_terminates, head_terminates_of_mem, head_think, head_terminates_of_get?_terminates
inhabited 📖	CompOp	—
join 📖	CompOp	11 math math: liftRel_join, map_join, join_ret, join_append, destruct_join, join_congr, join_join, join_think, join_cons, join_map_ret, join_nil
map 📖	CompOp	16 math math: map_congr, map_comp, map_think, map_cons, map_join, destruct_map, liftRel_map, bind_ret, Computation.map_parallel, mem_map, map_ret, map_append, join_join, map_nil, join_map_ret, map_id
membership 📖	CompOp	8 math math: get?_mem, Computation.exists_of_mem_parallel, eq_or_mem_iff_mem, notMem_nil, mem_congr, mem_cons_iff, mem_think, mem_cons
monad 📖	CompOp	—
nil 📖	CompOp	14 math math: seq_destruct_nil, head_nil, toList'_nil, tail_nil, ofList_nil, destruct_nil, liftRel_nil, map_nil, nil_append, notMem_nil, toList_nil, append_nil, join_nil, dropn_nil
ofList 📖	CompOp	3 math math: toList_ofList, ofList_cons, ofList_nil
ofSeq 📖	CompOp	7 math math: destruct_ofSeq, head_ofSeq, dropn_ofSeq, productive_ofSeq, tail_ofSeq, toSeq_ofSeq, get?_ofSeq
ofStream 📖	CompOp	—
recOn 📖	CompOp	—
ret 📖	CompOp	5 math math: join_ret, bind_ret, map_ret, join_map_ret, ret_bind
tail 📖	CompOp	9 math math: productive_tail, get?_tail, tail_nil, tail_think, tail_congr, tail_ofSeq, dropn_tail, destruct_tail, tail_cons
think 📖	CompOp	16 math math: seq_destruct_think, flatten_think, map_think, dropn_think, think_congr, tail_think, liftRel_think_right, join_think, join_cons, liftRel_think_left, mem_think, toList'_think, destruct_think, think_equiv, head_think, think_append
toList 📖	CompOp	7 math math: toList_terminates, toList'_map, length_eq_map, toList_ofList, IsFinite.out, toList_cons, toList_nil

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
append_assoc 📖	mathematical	—	append	—	Stream'.Seq.append_assoc
append_nil 📖	mathematical	—	append nil	—	Stream'.Seq.append_nil
cons_append 📖	mathematical	—	append cons	—	Stream'.Seq.cons_append
destruct_append 📖	mathematical	—	destruct append Computation.bind Stream'.WSeq destruct_append.aux	—	Computation.eq_of_bisim nil_append destruct_nil Computation.ret_bind destruct_cons destruct_think Computation.destruct_think cons_append think_append Computation.think_bind
destruct_cons 📖	mathematical	—	destruct cons Computation.pure Stream'.WSeq	—	Computation.destruct_eq_pure Computation.corec_eq Stream'.Seq.destruct_cons
destruct_dropn 📖	mathematical	—	destruct drop Computation Computation.instBind Stream'.WSeq drop.aux	—	Computation.bind_pure' dropn_tail destruct_tail Computation.instLawfulMonad
destruct_flatten 📖	mathematical	—	destruct flatten Computation Computation.instBind Stream'.WSeq	—	Computation.eq_of_bisim flatten_pure Computation.ret_bind flatten_think destruct_think Computation.destruct_think Computation.think_bind
destruct_join 📖	mathematical	—	destruct join Computation.bind Stream'.WSeq destruct_join.aux	—	Computation.eq_of_bisim join_nil destruct_nil Computation.ret_bind join_cons destruct_think Computation.destruct_think destruct_cons join_think Computation.think_bind
destruct_map 📖	mathematical	—	destruct map Computation.map Stream'.WSeq	—	Computation.eq_of_bisim destruct_nil map_cons destruct_cons map_think destruct_think Computation.destruct_think Computation.map_think
destruct_nil 📖	mathematical	—	destruct nil Computation.pure Stream'.WSeq	—	Computation.destruct_eq_pure
destruct_ofSeq 📖	mathematical	—	destruct ofSeq Computation.pure Stream'.WSeq Stream'.Seq.tail Stream'.Seq.head	—	Computation.destruct_eq_pure Computation.corec_eq Stream'.Seq.map_get? Stream'.Seq.map_tail
destruct_some_of_destruct_tail_some 📖	—	Stream'.WSeq Computation Computation.instMembership destruct tail	—	—	Computation.exists_of_mem_bind destruct_flatten Computation.exists_of_mem_map Computation.mem_unique destruct_nil Computation.ret_mem
destruct_tail 📖	mathematical	—	destruct tail Computation Computation.instBind Stream'.WSeq tail.aux	—	destruct_flatten Computation.instLawfulMonad destruct_nil
destruct_terminates_of_get?_terminates 📖	mathematical	—	Computation.Terminates Stream'.WSeq destruct	—	head_terminates_iff head_terminates_of_get?_terminates
destruct_think 📖	mathematical	—	destruct think Computation.think Stream'.WSeq	—	Computation.destruct_eq_think Computation.corec_eq Stream'.Seq.destruct_cons
dropn_add 📖	mathematical	—	drop	—	—
dropn_cons 📖	mathematical	—	drop cons	—	tail_cons
dropn_nil 📖	mathematical	—	drop nil	—	tail_nil
dropn_ofSeq 📖	mathematical	—	drop ofSeq Stream'.Seq.drop	—	tail_ofSeq
dropn_tail 📖	mathematical	—	drop tail	—	dropn_add
dropn_think 📖	mathematical	—	drop think	—	tail_think
eq_or_mem_iff_mem 📖	mathematical	Stream'.WSeq Computation Computation.instMembership destruct	membership	—	destruct_nil destruct_cons Stream'.eq_or_mem_of_mem_cons Stream'.mem_cons Stream'.mem_cons_of_mem destruct_think Computation.destruct_think
exists_dropn_of_mem 📖	mathematical	Stream'.WSeq membership	Computation Computation.instMembership destruct drop	—	exists_get?_of_mem head_terminates_iff Computation.mem_unique Computation.mem_map
exists_get?_of_mem 📖	mathematical	Stream'.WSeq membership	Computation Computation.instMembership get?	—	mem_rec_on head_cons Computation.ret_mem dropn_cons dropn_think head_think Computation.think_mem
exists_of_mem_bind 📖	—	Stream'.WSeq membership bind	—	—	exists_of_mem_join exists_of_mem_map
exists_of_mem_join 📖	—	Stream'.WSeq membership join	—	—	mem_rec_on join_nil append_nil seq_destruct_cons join_cons nil_append seq_destruct_think join_think cons_append think_append notMem_nil
exists_of_mem_map 📖	—	Stream'.WSeq membership map	—	—	Stream'.Seq.exists_of_mem_map
flatten_pure 📖	mathematical	—	flatten Computation.pure Stream'.WSeq	—	Stream'.Seq.eq_of_bisim Stream'.Seq.corec_eq
flatten_think 📖	mathematical	—	flatten Computation.think Stream'.WSeq think	—	Stream'.Seq.destruct_eq_cons Stream'.Seq.corec_eq Computation.destruct_think
get?_add 📖	mathematical	—	get? drop	—	dropn_add
get?_mem 📖	mathematical	Computation Computation.instMembership get?	Stream'.WSeq membership	—	Computation.exists_of_mem_map eq_or_mem_iff_mem mem_of_mem_tail get?_tail
get?_ofSeq 📖	mathematical	—	get? ofSeq Computation.pure Stream'.Seq.get?	—	dropn_ofSeq head_ofSeq Stream'.Seq.head_dropn
get?_tail 📖	mathematical	—	get? tail	—	dropn_tail
get?_terminates_le 📖	mathematical	—	Computation.Terminates get?	—	head_terminates_of_head_tail_terminates
head_cons 📖	mathematical	—	head cons Computation.pure	—	destruct_cons
head_nil 📖	mathematical	—	head nil Computation.pure	—	destruct_nil
head_ofSeq 📖	mathematical	—	head ofSeq Computation.pure Stream'.Seq.head	—	destruct_ofSeq
head_some_of_get?_some 📖	mathematical	Computation Computation.instMembership get?	head	—	head_some_of_head_tail_some
head_some_of_head_tail_some 📖	—	Computation Computation.instMembership head tail	—	—	Computation.exists_of_mem_map destruct_some_of_destruct_tail_some Computation.mem_map
head_terminates_iff 📖	mathematical	—	Computation.Terminates head Stream'.WSeq destruct	—	Computation.terminates_map_iff
head_terminates_of_get?_terminates 📖	mathematical	—	Computation.Terminates head	—	get?_terminates_le
head_terminates_of_head_tail_terminates 📖	mathematical	—	Computation.Terminates head	—	head_terminates_iff Computation.exists_of_mem_bind destruct_flatten Computation.instLawfulMonad Computation.terminates_of_mem
head_terminates_of_mem 📖	mathematical	Stream'.WSeq membership	Computation.Terminates head	—	exists_get?_of_mem head_terminates_of_get?_terminates
head_think 📖	mathematical	—	head think Computation.think	—	destruct_think Computation.map_think
join_cons 📖	mathematical	—	join cons Stream'.WSeq think append	—	Stream'.Seq.map_cons Stream'.Seq.join_cons
join_nil 📖	mathematical	—	join nil Stream'.WSeq	—	Stream'.Seq.join_nil
join_think 📖	mathematical	—	join think Stream'.WSeq	—	Stream'.Seq.map_cons Stream'.Seq.join_cons Stream'.Seq.nil_append
map_append 📖	mathematical	—	map append	—	Stream'.Seq.map_append
map_comp 📖	mathematical	—	map	—	Stream'.Seq.map_comp
map_cons 📖	mathematical	—	map cons	—	Stream'.Seq.map_cons
map_id 📖	mathematical	—	map	—	Stream'.Seq.map_id
map_join 📖	mathematical	—	map join Stream'.WSeq	—	Stream'.Seq.eq_of_bisim nil_append join_nil join_cons map_think map_append seq_destruct_think map_cons join_think cons_append seq_destruct_cons think_append
map_nil 📖	mathematical	—	map nil	—	—
map_ret 📖	mathematical	—	map ret	—	ofList_cons map_cons
map_think 📖	mathematical	—	map think	—	Stream'.Seq.map_cons
mem_append_left 📖	mathematical	Stream'.WSeq membership	append	—	Stream'.Seq.mem_append_left
mem_cons 📖	mathematical	—	Stream'.WSeq membership cons	—	mem_cons_iff
mem_cons_iff 📖	mathematical	—	Stream'.WSeq membership cons	—	eq_or_mem_iff_mem destruct_cons
mem_cons_of_mem 📖	mathematical	Stream'.WSeq membership	cons	—	mem_cons_iff
mem_map 📖	mathematical	Stream'.WSeq membership	map	—	Stream'.Seq.mem_map
mem_of_mem_dropn 📖	—	Stream'.WSeq membership drop	—	—	mem_of_mem_tail
mem_of_mem_tail 📖	—	Stream'.WSeq membership tail	—	—	tail_nil tail_cons tail_think
mem_rec_on 📖	—	Stream'.WSeq membership cons think	—	—	Stream'.Seq.mem_rec_on
mem_think 📖	mathematical	—	Stream'.WSeq membership think	—	Stream'.eq_or_mem_of_mem_cons Stream'.mem_cons_of_mem
nil_append 📖	mathematical	—	append nil	—	Stream'.Seq.nil_append
notMem_nil 📖	mathematical	—	Stream'.WSeq membership nil	—	Stream'.Seq.notMem_nil
ofList_cons 📖	mathematical	—	ofList cons	—	Stream'.Seq.ofList_cons Stream'.Seq.map_cons
ofList_nil 📖	mathematical	—	ofList nil	—	—
of_mem_append 📖	—	Stream'.WSeq membership append	—	—	Stream'.Seq.of_mem_append
seq_destruct_cons 📖	mathematical	—	Stream'.Seq.destruct cons Stream'.WSeq	—	Stream'.Seq.destruct_cons
seq_destruct_nil 📖	mathematical	—	Stream'.Seq.destruct nil Stream'.Seq1	—	—
seq_destruct_think 📖	mathematical	—	Stream'.Seq.destruct think Stream'.WSeq	—	Stream'.Seq.destruct_cons
tail_cons 📖	mathematical	—	tail cons	—	destruct_cons Computation.map_pure' flatten_pure
tail_nil 📖	mathematical	—	tail nil	—	destruct_nil Computation.map_pure' flatten_pure
tail_ofSeq 📖	mathematical	—	tail ofSeq Stream'.Seq.tail	—	destruct_ofSeq Computation.map_pure' flatten_pure Stream'.Seq.head_cons
tail_think 📖	mathematical	—	tail think	—	destruct_think Computation.map_think' flatten_think
think_append 📖	mathematical	—	append think	—	Stream'.Seq.cons_append
toList'_cons 📖	mathematical	—	Stream'.WSeq Stream'.Seq.destruct cons Computation.think	—	Computation.destruct_eq_think Computation.corec_eq Stream'.Seq.destruct_cons
toList'_map 📖	mathematical	—	Stream'.WSeq Stream'.Seq.destruct Computation Computation.instAlternativeComputation toList	—	Computation.eq_of_bisim Computation.corec_eq Computation.destruct_map Stream'.Seq.destruct_cons
toList'_nil 📖	mathematical	—	Stream'.WSeq Stream'.Seq.destruct nil Computation.pure	—	Computation.destruct_eq_pure
toList'_think 📖	mathematical	—	Stream'.WSeq Stream'.Seq.destruct think Computation.think	—	Computation.destruct_eq_think Computation.corec_eq Stream'.Seq.destruct_cons
toList_cons 📖	mathematical	—	toList cons Computation.think Computation Computation.instAlternativeComputation	—	Computation.destruct_eq_think toList'_cons Computation.destruct_think toList'_map
toList_nil 📖	mathematical	—	toList nil Computation.pure	—	Computation.destruct_eq_pure
toList_ofList 📖	mathematical	—	Computation Computation.instMembership toList ofList	—	toList_nil ofList_cons toList_cons Computation.think_mem Computation.mem_map

Stream'.WSeq.destruct_append

Definitions

Name	Category	Theorems
aux 📖	CompOp	1 math math: Stream'.WSeq.destruct_append

Stream'.WSeq.destruct_join

Definitions

Name	Category	Theorems
aux 📖	CompOp	1 math math: Stream'.WSeq.destruct_join

Stream'.WSeq.drop

Definitions

Name	Category	Theorems
aux 📖	CompOp	2 math math: aux_none, Stream'.WSeq.destruct_dropn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aux_none 📖	mathematical	—	aux Stream'.WSeq Computation.pure	—	Computation.ret_bind

Stream'.WSeq.tail

Definitions

Name	Category	Theorems
aux 📖	CompOp	1 math math: Stream'.WSeq.destruct_tail

---

← Back to Index