Do_until_alternate with_

Definitions:

[]→⊤, []→boolean, []→⊤
Source: /avail/Avail/Foundation/Control Structures
Categories: Control Structures, Loops
Conditional loop with alternation. Invoke action and then predicate. If predicate answers false, then invoke between. Then repeat.
Position Name Type Description
Parameters
1 action []→⊤ The function to apply once and then again repeatedly while predicate answers false.
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 @restricts , []→⊤'s type
Source: /avail/Avail/Foundation/Control Structures
If action does not terminate or predicate certainly answers false, then answer ⊥ (because the loop will run forever).
Type Description
Parameter Types
[]→⊤'s type @restricts []→boolean's type"
[]→⊤'s type