While_do_

Definitions:

[]→boolean, []→⊤
Source: /avail/Avail/Foundation/Control Structures
Categories: Control Structures, Loops
Basic conditional loop. Invoke predicate. If predicate answers true, then invoke action and repeat.
Position Name Type Description
Parameters
1 predicate []→boolean The function that guards repeated application of action.
2 action []→⊤ The function to apply whenever predicate answers true.
Returns ⊤

Semantic restrictions:

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