Idris2Doc : Chem.Atom

Chem.Atom

(source)

Definitions

record Atom : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type
  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)
.elem : Atom el chg pos rad hyd tpe chr lbl -> el
Totality: total
Visibility: public export
elem : Atom el chg pos rad hyd tpe chr lbl -> el
Totality: total
Visibility: public export
.charge : Atom el chg pos rad hyd tpe chr lbl -> chg
Totality: total
Visibility: public export
charge : Atom el chg pos rad hyd tpe chr lbl -> chg
Totality: total
Visibility: public export
.position : Atom el chg pos rad hyd tpe chr lbl -> pos
Totality: total
Visibility: public export
position : Atom el chg pos rad hyd tpe chr lbl -> pos
Totality: total
Visibility: public export
.radical : Atom el chg pos rad hyd tpe chr lbl -> rad
Totality: total
Visibility: public export
radical : Atom el chg pos rad hyd tpe chr lbl -> rad
Totality: total
Visibility: public export
.hydrogen : Atom el chg pos rad hyd tpe chr lbl -> hyd
Totality: total
Visibility: public export
hydrogen : Atom el chg pos rad hyd tpe chr lbl -> hyd
Totality: total
Visibility: public export
.type : Atom el chg pos rad hyd tpe chr lbl -> tpe
Totality: total
Visibility: public export
type : Atom el chg pos rad hyd tpe chr lbl -> tpe
Totality: total
Visibility: public export
.chirality : Atom el chg pos rad hyd tpe chr lbl -> chr
Totality: total
Visibility: public export
chirality : Atom el chg pos rad hyd tpe chr lbl -> chr
Totality: total
Visibility: public export
.label : Atom el chg pos rad hyd tpe chr lbl -> lbl
Totality: total
Visibility: public export
label : Atom el chg pos rad hyd tpe chr lbl -> lbl
Totality: total
Visibility: public export
interface HasMolecularMass : Type -> Type
Parameters: a
Methods:
molecularMass : a -> MolecularMass
exactMolecularMass : a -> MolecularMass

Implementations:
HasMolecularMass NoH
HasMolecularMass HCount
HasMolarMass e => HasMolecularMass h => HasMolecularMass (Atom e c p r h t ch x)
molecularMass : HasMolecularMass a => a -> MolecularMass
Totality: total
Visibility: public export
exactMolecularMass : HasMolecularMass a => a -> MolecularMass
Totality: total
Visibility: public export