Chem.Elem

Reexports

Definitions

data Elem : Type

  The chemical elements encoded as an enum type

Totality: total
Visibility: public export
Constructors:

H : Elem

He : Elem

Li : Elem

Be : Elem

B : Elem

C : Elem

N : Elem

O : Elem

F : Elem

Ne : Elem

Na : Elem

Mg : Elem

Al : Elem

Si : Elem

P : Elem

S : Elem

Cl : Elem

Ar : Elem

K : Elem

Ca : Elem

Sc : Elem

Ti : Elem

V : Elem

Cr : Elem

Mn : Elem

Fe : Elem

Co : Elem

Ni : Elem

Cu : Elem

Zn : Elem

Ga : Elem

Ge : Elem

As : Elem

Se : Elem

Br : Elem

Kr : Elem

Rb : Elem

Sr : Elem

Y : Elem

Zr : Elem

Nb : Elem

Mo : Elem

Tc : Elem

Ru : Elem

Rh : Elem

Pd : Elem

Ag : Elem

Cd : Elem

In : Elem

Sn : Elem

Sb : Elem

Te : Elem

I : Elem

Xe : Elem

Cs : Elem

Ba : Elem

La : Elem

Ce : Elem

Pr : Elem

Nd : Elem

Pm : Elem

Sm : Elem

Eu : Elem

Gd : Elem

Tb : Elem

Dy : Elem

Ho : Elem

Er : Elem

Tm : Elem

Yb : Elem

Lu : Elem

Hf : Elem

Ta : Elem

W : Elem

Re : Elem

Os : Elem

Ir : Elem

Pt : Elem

Au : Elem

Hg : Elem

Tl : Elem

Pb : Elem

Bi : Elem

Po : Elem

At : Elem

Rn : Elem

Fr : Elem

Ra : Elem

Ac : Elem

Th : Elem

Pa : Elem

U : Elem

Np : Elem

Pu : Elem

Am : Elem

Cm : Elem

Bk : Elem

Cf : Elem

Es : Elem

Fm : Elem

Md : Elem

No : Elem

Lr : Elem

Rf : Elem

Db : Elem

Sg : Elem

Bh : Elem

Hs : Elem

Mt : Elem

Ds : Elem

Rg : Elem

Cn : Elem

Nh : Elem

Fl : Elem

Mc : Elem

Lv : Elem

Ts : Elem

Og : Elem

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

Cast AromElem Elem

Cast Elem AromElem

Cast Isotope Elem

Cast Elem Isotope

Cast AromIsotope Elem

Cast Elem AromIsotope

Eq Elem

Finite Elem

HasMolarMass Elem

Interpolation Elem

Ord Elem

Show Elem

0 indexLemma : (e : Elem) -> IsAtomicNr (conIndexElem e + 1)

  This is a proof that we can safely compute an atomic number
  from each element's index

Totality: total
Visibility: export

atomicNr : Elem -> AtomicNr

  Compute the atomic number of an element

Totality: total
Visibility: public export

fromAtomicNr : AtomicNr -> Elem

  Compute the element from an atomic number

Totality: total
Visibility: public export

symbol : Elem -> String

  Return the chemical symbol of an element.

Totality: total
Visibility: public export

isNobleGas : Elem -> Bool

Totality: total
Visibility: export

isHalogen : Elem -> Bool

Totality: total
Visibility: export

isNonmetal : Elem -> Bool

Totality: total
Visibility: export

isMetalloid : Elem -> Bool

Totality: total
Visibility: export

isMetal : Elem -> Bool

Totality: total
Visibility: export

data ValidAromatic : Elem -> Bool -> Type

  Proof that only valid elements are marked as aromatic

Totality: total
Visibility: public export
Constructors:

VAB : ValidAromatic B True

VAC : ValidAromatic C True

VAN : ValidAromatic N True

VAO : ValidAromatic O True

VAP : ValidAromatic P True

VAS : ValidAromatic S True

VASe : ValidAromatic Se True

VAAs : ValidAromatic As True

VARest : ValidAromatic e False

record AromElem : Type

  An element paired with a boolean flag indicating whether the atom
  in question is part of an aromatic system.

Totality: total
Visibility: public export
Constructor: 

MkAE : (elem : Elem) -> (arom : Bool) -> {auto 0 _ : ValidAromatic elem arom} -> AromElem

Projections:

.arom : AromElem -> Bool

.elem : AromElem -> Elem

0 .prf : ({rec:0} : AromElem) -> ValidAromatic (elem {rec:0}) (arom {rec:0})

Hints:

Cast AromElem Elem

Cast Elem AromElem

Cast Isotope AromElem

Cast AromElem Isotope

Cast AromIsotope AromElem

Cast AromElem AromIsotope

Eq AromElem

Finite AromElem

Interpolation AromElem

Show AromElem

.elem : AromElem -> Elem

Totality: total
Visibility: public export

elem : AromElem -> Elem

Totality: total
Visibility: public export

.arom : AromElem -> Bool

Totality: total
Visibility: public export

arom : AromElem -> Bool

Totality: total
Visibility: public export

0 .prf : ({rec:0} : AromElem) -> ValidAromatic (elem {rec:0}) (arom {rec:0})

Totality: total
Visibility: public export

0 prf : ({rec:0} : AromElem) -> ValidAromatic (elem {rec:0}) (arom {rec:0})

Totality: total
Visibility: public export

nonAromElem : Elem -> AromElem

Totality: total
Visibility: public export

aromElem : (e : Elem) -> {auto 0 _ : ValidAromatic e True} -> AromElem

Totality: total
Visibility: public export