Idris2Doc : Chem.Atom

Chem.Atom

(source)

Definitions

recordAtom : 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->Atomelchgposradhydtpechrlbl

Projections:
.charge : Atomelchgposradhydtpechrlbl->chg
.chirality : Atomelchgposradhydtpechrlbl->chr
.elem : Atomelchgposradhydtpechrlbl->el
.hydrogen : Atomelchgposradhydtpechrlbl->hyd
.label : Atomelchgposradhydtpechrlbl->lbl
.position : Atomelchgposradhydtpechrlbl->pos
.radical : Atomelchgposradhydtpechrlbl->rad
.type : Atomelchgposradhydtpechrlbl->tpe

Hints:
CasteElem=>Cast (AtomecprNoHtchl) Formula
CasteElem=>Cast (AtomecprHCounttchl) Formula
Eqel=>Eqchg=>Eqpos=>Eqrad=>Eqhyd=>Eqtpe=>Eqchr=>Eqlbl=>Eq (Atomelchgposradhydtpechrlbl)
Foldable (Atomecprhtch)
Functor (Atomecprhtch)
HasMolarMasse=>HasMolecularMassh=>HasMolecularMass (Atomecprhtchx)
Showel=>Showchg=>Showpos=>Showrad=>Showhyd=>Showtpe=>Showchr=>Showlbl=>Show (Atomelchgposradhydtpechrlbl)
Traversable (Atomecprhtch)
.elem : Atomelchgposradhydtpechrlbl->el
Totality: total
Visibility: public export
elem : Atomelchgposradhydtpechrlbl->el
Totality: total
Visibility: public export
.charge : Atomelchgposradhydtpechrlbl->chg
Totality: total
Visibility: public export
charge : Atomelchgposradhydtpechrlbl->chg
Totality: total
Visibility: public export
.position : Atomelchgposradhydtpechrlbl->pos
Totality: total
Visibility: public export
position : Atomelchgposradhydtpechrlbl->pos
Totality: total
Visibility: public export
.radical : Atomelchgposradhydtpechrlbl->rad
Totality: total
Visibility: public export
radical : Atomelchgposradhydtpechrlbl->rad
Totality: total
Visibility: public export
.hydrogen : Atomelchgposradhydtpechrlbl->hyd
Totality: total
Visibility: public export
hydrogen : Atomelchgposradhydtpechrlbl->hyd
Totality: total
Visibility: public export
.type : Atomelchgposradhydtpechrlbl->tpe
Totality: total
Visibility: public export
type : Atomelchgposradhydtpechrlbl->tpe
Totality: total
Visibility: public export
.chirality : Atomelchgposradhydtpechrlbl->chr
Totality: total
Visibility: public export
chirality : Atomelchgposradhydtpechrlbl->chr
Totality: total
Visibility: public export
.label : Atomelchgposradhydtpechrlbl->lbl
Totality: total
Visibility: public export
label : Atomelchgposradhydtpechrlbl->lbl
Totality: total
Visibility: public export
interfaceHasMolecularMass : Type->Type
Parameters: a
Methods:
molecularMass : a->MolecularMass
exactMolecularMass : a->MolecularMass

Implementations:
HasMolecularMassNoH
HasMolecularMassHCount
HasMolarMasse=>HasMolecularMassh=>HasMolecularMass (Atomecprhtchx)
molecularMass : HasMolecularMassa=>a->MolecularMass
Totality: total
Visibility: public export
exactMolecularMass : HasMolecularMassa=>a->MolecularMass
Totality: total
Visibility: public export