- data EraseDirection : Type
- Totality: total
Constructors:
- Start : EraseDirection
- End : EraseDirection
- All : EraseDirection
- cursorBack : Nat -> String
Moves the cursor n columns back.
If the cursor is at the edge of the screen it has no effect.
Totality: total- cursorBack1 : String
- Totality: total
- cursorDown : Nat -> String
Moves the cursor n columns down.
If the cursor is at the edge of the screen it has no effect.
Totality: total- cursorDown1 : String
- Totality: total
- cursorForward : Nat -> String
Moves the cursor n columns forward.
If the cursor is at the edge of the screen it has no effect.
Totality: total- cursorForward1 : String
- Totality: total
- cursorMove : Nat -> Nat -> String
Moves the cursor at an arbitrary line and column.
Both lines and columns start at 1.
Totality: total- cursorNextLine : Nat -> String
Moves the cursor at the beginning of n lines down.
If the cursor is at the edge of the screen it has no effect.
Totality: total- cursorNextLine1 : String
- Totality: total
- cursorPrevLine : Nat -> String
Moves the cursor at the beginning of n lines up.
If the cursor is at the edge of the screen it has no effect.
Totality: total- cursorPrevLine1 : String
- Totality: total
- cursorUp : Nat -> String
Moves the cursor n columns up.
If the cursor is at the edge of the screen it has no effect.
Totality: total- cursorUp1 : String
- Totality: total
- eraseLine : EraseDirection -> String
Clears part of the line.
Totality: total- eraseScreen : EraseDirection -> String
Clears part of the screen.
Totality: total- scrollDown : Nat -> String
Scrolls the whole screen down by n lines.
Totality: total- scrollDown1 : String
- Totality: total
- scrollUp : Nat -> String
Scrolls the whole screen up by n lines.
Totality: total- scrollUp1 : String
- Totality: total