Idris2Doc : Syntax.StringDiagram.Arrow

Syntax.StringDiagram.Arrow

(source)
Reexports
import public Control.Monad.State
import public Control.Applicative.Const
import public Control.Arrow
import public Control.Category.Core
import public Language.Reflection
import public Data.Wrap0
Definitions
arrowImpl : TTImp -> Elab TTImp
  Totality: total
  Visibility: export
arrowDo : {auto 0 _ : Arrow arr} -> TTImp -> Elab (arr (W0 a) (W0 b))
  Enter arrow notation.
  
  This elaboration script must be specifically invoked with
  `%runElab`. The category is inferred from the return type.

  Totality: total
  Visibility: export