Do_while_

Definitions:

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

Semantic restrictions:

[]→⊤'s type, []→boolean'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