Stellar.API.Kleene

Definitions

data StarShp : API -> Type

Totality: total
Visibility: public export
Constructors:

Done : StarShp c

More : Ex c (StarShp c) -> StarShp c

data StarPos : (c : API) -> StarShp c -> Type

Totality: total
Visibility: public export
Constructors:

StarU : StarPos c Done

StarM : (x : c .response x1) -> StarPos c (x2 x) -> StarPos c (More (MkEx x1 x2))

.star : API -> API

Totality: total
Visibility: public export

Kleene : API -> API

Totality: total
Visibility: public export

mapStarShp : a =&> b -> StarShp a -> StarShp b

Totality: total
Visibility: public export

mapStarPos : (mor : a =&> b) -> (x : StarShp a) -> StarPos b (mapStarShp mor x) -> StarPos a x

Totality: total
Visibility: public export

map_kleene : a =&> b -> a .star =&> b .star

Totality: total
Visibility: public export

join_star : StarShp (a .star) -> StarShp a

Totality: total
Visibility: public export

single : a .message -> StarShp a

Totality: total
Visibility: public export

pure_kleene : a =&> a .star

Totality: total
Visibility: public export

unit_kleene : End .star =&> End

Totality: total
Visibility: public export

kleeneCounit : a =&> End -> a .star =&> End

Totality: total
Visibility: export

runStar : a =&> b .star -> b =&> End -> a =&> End

Totality: total
Visibility: export