IdrisDoc: Chapter.StateMachines.StackOperationsChapter.StateMachines.StackOperations
- data StackCmd : (ty : Type) ->
(a : Type) ->
(inHeight : Nat) ->
(outHeight : Nat) ->
Type
- Push : a ->
StackCmd ()
a
height
(S height)
- Pop : StackCmd a
a
(S height)
height
- Top : StackCmd a
a
(S height)
(S height)
- GetStr : StackCmd String
a
height
height
- PutStr : String ->
StackCmd ()
a
height
height
- Pure : ty ->
StackCmd ty
a
height
height
- (>>=) : StackCmd a
elem
height1
height2 ->
(a ->
StackCmd b
elem
height2
height3) ->
StackCmd b
elem
height1
height3
- Fixity
- Left associative, precedence 5