import public Control.Category.Core
import public Control.Category.Functor
import public Control.Category.Monoidal
import public Control.Category.Braided
import public Data.Fin
import public Language.Reflection
import public Syntax.StringDiagram.UtilstringImpl : TTImp -> TTImp -> TTImp -> Elab TTImpExpand 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 `Braided` implementation the expansion will use.
string : (0 ten : (obj -> obj -> obj)) -> Braided cat ten i => TTImp -> Elab (cat a b)Enter string diagram notation (for `Braided`).
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.
NOTE: This notation is intended for use with symmetric monoidal
categories, and may be confusing if used in the non-symmetric
braided case. If your category is non-symmetric, it may be better
to use the string diagram notation for `Monoidal` and insert
explicit braiding calls.