Data.Container.Base.RoseTree.Definition

Definitions

data RoseTreeShape : (0 c : Cont) -> TensorMonoid c => Type

Totality: total
Visibility: public export
Constructors:

LeafS : {auto {conArg:8925} : TensorMonoid c} -> RoseTreeShape c

NodeS : {auto {conArg:8931} : TensorMonoid c} -> fullOf c (RoseTreeShape c) -> RoseTreeShape c

numLeaves : {auto {conArg:8942} : TensorMonoid c} -> Foldable (Ext c) => RoseTreeShape c -> Nat

Visibility: public export

numNodes : {auto {conArg:8991} : TensorMonoid c} -> Foldable (Ext c) => RoseTreeShape c -> Nat

Visibility: public export

data RoseTreePos : (0 c : Cont) -> {auto {conArg:9046} : TensorMonoid c} -> RoseTreeShape c -> Type

  Positions corresponding to both nodes and leaves within a RoseTreeShape

Totality: total
Visibility: public export
Constructors:

AtLeaf : {auto {conArg:9058} : TensorMonoid c} -> RoseTreePos c LeafS

AtNode : {auto {conArg:9067} : TensorMonoid c} -> RoseTreePos c (NodeS ts)

SubTree : {auto {conArg:9080} : TensorMonoid c} -> (ps : c .Pos (shapeExt ts)) -> RoseTreePos c (index ts ps) -> RoseTreePos c (NodeS ts)

data RoseTreePosNode : (0 c : Cont) -> {auto {conArg:9108} : TensorMonoid c} -> RoseTreeShape c -> Type

Totality: total
Visibility: public export
Constructors:

AtNode : {auto {conArg:9120} : TensorMonoid c} -> RoseTreePosNode c (NodeS ts)

SubTree : {auto {conArg:9133} : TensorMonoid c} -> (ps : c .Pos (shapeExt ts)) -> RoseTreePosNode c (index ts ps) -> RoseTreePosNode c (NodeS ts)

data RoseTreePosLeaf : (0 c : Cont) -> {auto {conArg:9161} : TensorMonoid c} -> RoseTreeShape c -> Type

Totality: total
Visibility: public export
Constructors:

AtLeaf : {auto {conArg:9173} : TensorMonoid c} -> RoseTreePosLeaf c LeafS

SubTree : {auto {conArg:9182} : TensorMonoid c} -> (ps : c .Pos (shapeExt ts)) -> RoseTreePosLeaf c (index ts ps) -> RoseTreePosLeaf c (NodeS ts)