Structures · Data types
Computation.Terminates
Terminates s asserts that the computation s eventually terminates with some value.
- Defined in
- Mathlib.Data.Seq.Computation
- Shape
- One type argument · adds term
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- List
- Option
How is a type an instance?
Loading the hierarchy index…
Assumed by28
- Computation.get
- Computation.length
- Computation.get_eq_of_mem
- Computation.get_mem
- Computation.results_of_terminates
- Computation.Results.length
- Computation.mem_of_promises
- Computation.results_of_terminates'
- Computation.terminates_parallel
- Computation.terminatesRecOn
- Stream'.WSeq.head_terminates_of_head_tail_terminates
- Computation.length_think
- Computation.Terminates.term
- Computation.eq_thinkN'
- Computation.length_bind
- Computation.get_eq_of_promises
- Computation.get_think
- Computation.think_terminates
- Computation.length_thinkN
- Computation.get_equiv
- Computation.terminates_map
- Computation.mem_of_get_eq
- Computation.thinkN_terminates
- Computation.terminates_bind
- Computation.get_bind
- Computation.get.congr_simp
- Computation.get_thinkN
- Computation.get_promises
Ancestors0
No ancestors.