Generic atom type
Depending on an atom's origin and use case, different
fields hold values of different types. Typically, if a
field holds no information of interest, the corresponding
type should be set to `Unit` (`()`).
@el : Element label. This can be `Elem`, `AromElem` or
a more general type that can be used for queries
for instance
@chg : Type representing the charge of an atom
@pos : Coordinates, representing the position of an atom
@rad : Type holding information about the atom being
a radical or not
@hyd : Implicit hydrogen count
@tpe : Atom type. This is used to describe not only
the chemical element but also the atom's connectivity
and, possibly, hybridisation
@chr : Chirality information
@lbl : Generic label holding additional information. This is
placed last, so that an atom becomes a `Traversable`
w.r.t. the label
Totality: total
Visibility: public export
Constructor: MkAtom : el -> chg -> pos -> rad -> hyd -> tpe -> chr -> lbl -> Atom el chg pos rad hyd tpe chr lbl
Projections:
.charge : Atom el chg pos rad hyd tpe chr lbl -> chg .chirality : Atom el chg pos rad hyd tpe chr lbl -> chr .elem : Atom el chg pos rad hyd tpe chr lbl -> el .hydrogen : Atom el chg pos rad hyd tpe chr lbl -> hyd .label : Atom el chg pos rad hyd tpe chr lbl -> lbl .position : Atom el chg pos rad hyd tpe chr lbl -> pos .radical : Atom el chg pos rad hyd tpe chr lbl -> rad .type : Atom el chg pos rad hyd tpe chr lbl -> tpe
Hints:
Cast e Elem => Cast (Atom e c p r NoH t ch l) Formula Cast e Elem => Cast (Atom e c p r HCount t ch l) Formula Eq el => Eq chg => Eq pos => Eq rad => Eq hyd => Eq tpe => Eq chr => Eq lbl => Eq (Atom el chg pos rad hyd tpe chr lbl) Foldable (Atom e c p r h t ch) Functor (Atom e c p r h t ch) HasMolarMass e => HasMolecularMass h => HasMolecularMass (Atom e c p r h t ch x) Show el => Show chg => Show pos => Show rad => Show hyd => Show tpe => Show chr => Show lbl => Show (Atom el chg pos rad hyd tpe chr lbl) Traversable (Atom e c p r h t ch)