Productive

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

Statistics

Metric	Count
Definitions Productive, toSeq	2
Theorems get?_terminates, get?_terminates, head_terminates, productive_congr, productive_dropn, productive_iff, productive_ofSeq, productive_tail, toSeq_ofSeq	9
Total	11

Stream'.WSeq

Definitions

Name	Category	Theorems
Productive 📖	CompData	5 math math: productive_iff, productive_dropn, productive_tail, productive_ofSeq, productive_congr
toSeq 📖	CompOp	1 math math: toSeq_ofSeq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
get?_terminates 📖	mathematical	—	Computation.Terminates get?	—	Productive.get?_terminates
head_terminates 📖	mathematical	—	Computation.Terminates head	—	get?_terminates
productive_congr 📖	mathematical	Equiv	Productive	—	Computation.terminates_congr get?_congr
productive_dropn 📖	mathematical	—	Productive drop	—	get?_add get?_terminates
productive_iff 📖	mathematical	—	Productive Computation.Terminates get?	—	Productive.get?_terminates
productive_ofSeq 📖	mathematical	—	Productive ofSeq	—	get?_ofSeq Computation.ret_terminates
productive_tail 📖	mathematical	—	Productive tail	—	get?_tail get?_terminates
toSeq_ofSeq 📖	mathematical	—	toSeq ofSeq productive_ofSeq	—	productive_ofSeq Computation.get_eq_of_mem get?_terminates get?_ofSeq Computation.ret_mem

Stream'.WSeq.Productive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
get?_terminates 📖	mathematical	—	Computation.Terminates Stream'.WSeq.get?	—	—

---

← Back to Index