Syntax.StringDiagram.Util

Definitions

parseListOrSing : TTImp -> Elab (List String)

Totality: total
Visibility: export

parseListOrSingPat : TTImp -> Elab (List (Maybe String))

Totality: total
Visibility: export

parseLam : TTImp -> Elab (List (Maybe String), TTImp)

Totality: total
Visibility: export

record SDiagramStep : Type

Totality: total
Visibility: public export
Constructor: 

MkSDStep : List String -> TTImp -> List (Maybe String) -> SDiagramStep

Projections:

.inputs : SDiagramStep -> List String

.mor : SDiagramStep -> TTImp

.outputs : SDiagramStep -> List (Maybe String)

.inputs : SDiagramStep -> List String

Totality: total
Visibility: public export

inputs : SDiagramStep -> List String

Totality: total
Visibility: public export

.mor : SDiagramStep -> TTImp

Totality: total
Visibility: public export

mor : SDiagramStep -> TTImp

Totality: total
Visibility: public export

.outputs : SDiagramStep -> List (Maybe String)

Totality: total
Visibility: public export

outputs : SDiagramStep -> List (Maybe String)

Totality: total
Visibility: public export

record SDiagram : Type

Totality: total
Visibility: public export
Constructor: 

MkSDiagram : List (Maybe String) -> List SDiagramStep -> List String -> SDiagram

Projections:

.inputs : SDiagram -> List (Maybe String)

.outputs : SDiagram -> List String

.steps : SDiagram -> List SDiagramStep

.inputs : SDiagram -> List (Maybe String)

Totality: total
Visibility: public export

inputs : SDiagram -> List (Maybe String)

Totality: total
Visibility: public export

.steps : SDiagram -> List SDiagramStep

Totality: total
Visibility: public export

steps : SDiagram -> List SDiagramStep

Totality: total
Visibility: public export

.outputs : SDiagram -> List String

Totality: total
Visibility: public export

outputs : SDiagram -> List String

Totality: total
Visibility: public export

parseDiagram : TTImp -> Elab SDiagram

Totality: total
Visibility: export