Idris2Doc : Data.Container.Applicative.TreeUtils

Data.Container.Applicative.TreeUtils

(source)
Definitions
data RoseTreeShape : (c : Cont) -> TensorMonoid c => Type
  Totality: total
  Visibility: public export
  Constructors:
  
LeafS : {auto {conArg:4787} : TensorMonoid c} -> RoseTreeShape c
  
NodeS : {auto {conArg:4793} : TensorMonoid c} -> fullOf c (RoseTreeShape c) -> RoseTreeShape c
numLeaves : {auto {conArg:4804} : TensorMonoid c} -> Foldable (Ext c) => RoseTreeShape c -> Nat
  Visibility: public export
numNodes : {auto {conArg:4857} : TensorMonoid c} -> Foldable (Ext c) => RoseTreeShape c -> Nat
  Visibility: public export
data RoseTreePos : (c : Cont) -> {auto {conArg:4917} : TensorMonoid c} -> RoseTreeShape c -> Type
  Positions corresponding to both nodes and leaves within a RoseTreeShape

  Totality: total
  Visibility: public export
  Constructors:
  
AtLeaf : {auto {conArg:4929} : TensorMonoid c} -> RoseTreePos c LeafS
  
AtNode : {auto {conArg:4939} : TensorMonoid c} -> RoseTreePos c (NodeS ts)
  
SubTree : {auto {conArg:4953} : TensorMonoid c} -> (ps : c .Pos (shapeExt ts)) -> RoseTreePos c (index ts ps) -> RoseTreePos c (NodeS ts)
data RoseTreePosNode : (c : Cont) -> {auto {conArg:4982} : TensorMonoid c} -> RoseTreeShape c -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
AtNode : {auto {conArg:4994} : TensorMonoid c} -> RoseTreePosNode c (NodeS ts)
  
SubTree : {auto {conArg:5008} : TensorMonoid c} -> (ps : c .Pos (shapeExt ts)) -> RoseTreePosNode c (index ts ps) -> RoseTreePosNode c (NodeS ts)
data RoseTreePosLeaf : (c : Cont) -> {auto {conArg:5037} : TensorMonoid c} -> RoseTreeShape c -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
AtLeaf : {auto {conArg:5049} : TensorMonoid c} -> RoseTreePosLeaf c LeafS
  
SubTree : {auto {conArg:5059} : TensorMonoid c} -> (ps : c .Pos (shapeExt ts)) -> RoseTreePosLeaf c (index ts ps) -> RoseTreePosLeaf c (NodeS ts)