Idris2Doc : Syntax.StringDiagram.Cartesian

Syntax.StringDiagram.Cartesian

(source)
Reexports
import public Control.Category.Core
import public Control.Category.Functor
import public Control.Category.Monoidal
import public Control.Category.Cartesian
import public Data.Fin
import public Language.Reflection
import public Syntax.StringDiagram.Util
Definitions
stringImpl : TTImp -> TTImp -> TTImp -> Elab TTImp
  Expand shortened string diagram notation into a full expression.
  
  This takes two additional parameters: `obj`, which is a wildcard
  expression used when passing objects as parameters, and `impl`,
  which is the `Cartesian` implementation the expansion will use.

  Totality: total
  Visibility: export
string : (0 ten : (obj -> obj -> obj)) -> Cartesian cat ten i => TTImp -> Elab (cat a b)
  Enter string diagram notation (for `Cartesian`).
  
  This elaboration script must be specifically invoked with
  `%runElab`. The category is inferred from the return type, but
  the tensor product must be passed as an explicit argument.

  Totality: total
  Visibility: export