Theorems · Definition · logic and foundations
Computation
Type u → Type u
Computation α is the type of unbounded computations returning α.
An element of Computation α is an infinite sequence of Option α such
that if f n = some a for some n then it is constantly some a after that.
- Defined in
- Mathlib.Data.Seq.Computation
- Cited by
- 182 results in Mathlib
- Foundations
- Depth 8 from the axioms, rests on 25 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Stream'proof · cited by 205
Cited by234
Results whose statement or proof uses this declaration.
- Computation.purestatement · cited by 61
- Computation.Terminatesstatement · cited by 48
- Computation.thinkstatement and proof · cited by 41
- Stream'.WSeq.destructstatement · cited by 41
- Computation.LiftRelstatement and proof · cited by 38
- Computation.destructstatement and proof · cited by 37
- Computation.bindstatement and proof · cited by 22
- Computation.Equivstatement and proof · cited by 21
- Computation.destruct_thinkstatement and proof · cited by 21
- Computation.mapstatement and proof · cited by 21
- Computation.Resultsstatement and proof · cited by 20
- Stream'.WSeq.get?statement · cited by 19
Showing the 200 most cited of 234.