CyBy.Draw.Internal.Atom

Definitions

record CDAtom : Type

  Atom type used in the application state of cyby-draw.
  
  This is a mol-file atom with perceived atom type paired with a role
  used for drawing.

Totality: total
Visibility: public export
Constructor: 

CA : Role -> MolAtomAT -> CDAtom

Projections:

.atom : CDAtom -> MolAtomAT

.role : CDAtom -> Role

Hints:

Cast CDAtom Role

Cast (Adj k b CDAtom) Role

Cast (Context k b CDAtom) Role

Cast CDAtom Elem

Eq CDAtom

GetPoint CDAtom

ModPoint CDAtom

ModRole CDAtom

Show CDAtom

.role : CDAtom -> Role

Totality: total
Visibility: public export

role : CDAtom -> Role

Totality: total
Visibility: public export

.atom : CDAtom -> MolAtomAT

Totality: total
Visibility: public export

atom : CDAtom -> MolAtomAT

Totality: total
Visibility: public export

group : CDAtom -> Maybe AtomGroup

Totality: total
Visibility: export

inAnyGroup : CDAtom -> Bool

Totality: total
Visibility: export

setGroup : AtomGroup -> CDAtom -> CDAtom

  Sets the given `AtomGroup` (abbreviation) at an atom

Totality: total
Visibility: export

clearGroup : Nat -> CDAtom -> CDAtom

  Unsets the abbreviation label of an atom if it belongs to
  the given group.

Totality: total
Visibility: export

inGroup : Nat -> CDAtom -> Bool

  True, if the given atom is part of the abbreviation with the given ID.

Totality: total
Visibility: export