While_do_alternate with_

Definitions:

[]→⊤, []→boolean, []→⊤
Source: /avail/Avail/Foundation/Control Structures
Categories: Control Structures, Loops
Conditional loop with alternation.
Position Name Type Description
Parameters
1 action []→⊤ The function to apply repeatedly while predicate answers true. Never invoked if predicate never answers true.
2 predicate []→boolean The function that guards repeated application of action.
3 between []→⊤ The function to apply between applications of action.
Returns ⊤

Semantic restrictions:

[]→⊤'s type, []→boolean's type, []→⊤'s type
Source: /avail/Avail/Foundation/Control Structures
If action does not terminate or predicate certainly answers true, then answer ⊥ (because the loop will run forever).
Type Description
Parameter Types
[]→⊤'s type
[]→boolean's type
[]→⊤'s type