From_to_do_

Definitions:

integer, extended integer, [⊥]→boolean
Source: /avail/Avail/Foundation/Control Structures
Categories: Control Structures, Loops
Counting loop with early exit support. Invoke action once for every consecutive number in the range established by start and end, aborting if action answers false after an iteration.
Position Name Type Description
Parameters
1 start integer The start value, inclusive.
2 end extended integer The end value, inclusive.
3 action [⊥]→boolean A function that accepts a value in the specified range. If it answers true, then continue to iterate; if it answers false, then terminate iteration early.
Returns ⊤
integer, extended integer, [⊥]→⊤
Source: /avail/Avail/Foundation/Control Structures
Categories: Control Structures, Loops
Counting loop with early exit support. Invoke action once for every consecutive number in the range established by start and end.
Position Name Type Description
Parameters
1 start integer The start value, inclusive.
2 end extended integer The end value, inclusive.
3 action [⊥]→⊤ A function that accepts a value in the specified range.
Returns ⊤

Semantic restrictions:

integer's type, extended integer's type, [⊥]→⊤'s type
Source: /avail/Avail/Foundation/Control Structures
If possible, then enforce that the specified function will accept all values in the implied range.
Type Description
Parameter Types
integer's type
extended integer's type
[⊥]→⊤'s type
integer's type, extended integer's type, [⊥]→boolean's type
Source: /avail/Avail/Foundation/Control Structures
If possible, then enforce that the specified function will accept all values in the implied range.
Type Description
Parameter Types
integer's type
extended integer's type
[⊥]→boolean's type