Geom.Gen2D.Types

Reexports

Definitions

0 Nodes : Nat -> Type

Totality: total
Visibility: public export

0 SnocNodes : Nat -> Type

Totality: total
Visibility: public export

data AttachPoint : Nat -> Type

Totality: total
Visibility: public export
Constructors:

None : AttachPoint k

Attach : Fin k -> Fin k -> AttachPoint k

Hints:

Eq (AttachPoint k)

Show (AttachPoint k)

0 SubgraphType : Bool -> Nat -> Type -> Type -> Type

Totality: total
Visibility: public export

record Component : Nat -> Type -> Type -> Type

  A component is a part of a molecular graph that will be placed
  as a single unit.
  
  Every componenent `c` except the first (the "main component")
  comes with an attachement point: A node in another component
  that will be placed before `c`.

Totality: total
Visibility: public export
Constructor: 

C : AttachPoint k -> List (Fin k) -> (isRing : Bool) -> SubgraphType isRing k e n -> Component k e n

Projections:

.attach : Component k e n -> AttachPoint k

.isRing : Component k e n -> Bool

.nodes : Component k e n -> List (Fin k)

.subgraph : ({rec:0} : Component k e n) -> SubgraphType (isRing {rec:0}) k e n

.attach : Component k e n -> AttachPoint k

Totality: total
Visibility: public export

attach : Component k e n -> AttachPoint k

Totality: total
Visibility: public export

.nodes : Component k e n -> List (Fin k)

Totality: total
Visibility: public export

nodes : Component k e n -> List (Fin k)

Totality: total
Visibility: public export

.isRing : Component k e n -> Bool

Totality: total
Visibility: public export

isRing : Component k e n -> Bool

Totality: total
Visibility: public export

.subgraph : ({rec:0} : Component k e n) -> SubgraphType (isRing {rec:0}) k e n

Totality: total
Visibility: public export

subgraph : ({rec:0} : Component k e n) -> SubgraphType (isRing {rec:0}) k e n

Totality: total
Visibility: public export

0 SnocComps : Nat -> Type -> Type -> Type

Totality: total
Visibility: public export

0 Comps : Nat -> Type -> Type -> Type

Totality: total
Visibility: public export

components : IGraph k e n -> List (Component k e n)

  Partitions the nodes of a graph into disjoint components,
  which will be placed individually in the given order.
  
  The first component to be placed will be the most complex
  cyclic system (if any) or the longest chain. All other
  components in the list are linked via an `AttachPoint` to
  a parent component, which will be placed first.

Totality: total
Visibility: export