Idris2Doc : Chem.Data

Chem.Data

(source)
Definitions
record ElemData : Type
  Additional data about the elements

  Totality: total
  Visibility: public export
  Constructor: 
ED : MolarMass -> MolarMass -> Double -> Maybe Double -> Maybe Double -> Maybe Double -> Maybe Double -> Maybe Double -> Maybe Double -> ElemData

  Projections:
  
.boilingpoint : ElemData -> Maybe Double
  
.electronAffinity : ElemData -> Maybe Double
  
.electronegativity : ElemData -> Maybe Double
  
.exactMass : ElemData -> MolarMass
  
.ionization : ElemData -> Maybe Double
  
.mass : ElemData -> MolarMass
  
.meltingpoint : ElemData -> Maybe Double
  
.radiusCovalent : ElemData -> Double
  
.radiusVDW : ElemData -> Maybe Double
.mass : ElemData -> MolarMass
  Totality: total
  Visibility: public export
mass : ElemData -> MolarMass
  Totality: total
  Visibility: public export
.exactMass : ElemData -> MolarMass
  Totality: total
  Visibility: public export
exactMass : ElemData -> MolarMass
  Totality: total
  Visibility: public export
.radiusCovalent : ElemData -> Double
  Totality: total
  Visibility: public export
radiusCovalent : ElemData -> Double
  Totality: total
  Visibility: public export
.radiusVDW : ElemData -> Maybe Double
  Totality: total
  Visibility: public export
radiusVDW : ElemData -> Maybe Double
  Totality: total
  Visibility: public export
.ionization : ElemData -> Maybe Double
  Totality: total
  Visibility: public export
ionization : ElemData -> Maybe Double
  Totality: total
  Visibility: public export
.electronAffinity : ElemData -> Maybe Double
  Totality: total
  Visibility: public export
electronAffinity : ElemData -> Maybe Double
  Totality: total
  Visibility: public export
.electronegativity : ElemData -> Maybe Double
  Totality: total
  Visibility: public export
electronegativity : ElemData -> Maybe Double
  Totality: total
  Visibility: public export
.boilingpoint : ElemData -> Maybe Double
  Totality: total
  Visibility: public export
boilingpoint : ElemData -> Maybe Double
  Totality: total
  Visibility: public export
.meltingpoint : ElemData -> Maybe Double
  Totality: total
  Visibility: public export
meltingpoint : ElemData -> Maybe Double
  Totality: total
  Visibility: public export
arrElemData : IArray 118 ElemData
  Array holding additional information about each element.

  Totality: total
  Visibility: export
0 conIndexLemma : (e : Elem) -> cast (conIndexElem e) < the Nat 118 = True
  Proof that the con index of an element is less than the natural number 118.
  
  This allows us to use elements (actually, their constructor index, which is
  the same at runtime) to safely index into the info arrays in this module.

  Totality: total
  Visibility: export
elemData : Elem -> ElemData
  Get additional information about an element.

  Totality: total
  Visibility: export
radiusCovalent : Elem -> Double
  Returns the covalent radius (in Angstrom) of an element.

  Totality: total
  Visibility: export
radiusVDW : Elem -> Maybe Double
  Returns the van der Waals radius (in Angstrom) of an element.

  Totality: total
  Visibility: export
ionization : Elem -> Maybe Double
  Returns the ionization energy (in ev) of an element.

  Totality: total
  Visibility: export
electronAffinity : Elem -> Maybe Double
  Returns the electron affinity energy (in ev) of an element.

  Totality: total
  Visibility: export
electronegativity : Elem -> Maybe Double
  Returns the Pauling electronegativity of an element.

  Totality: total
  Visibility: export
boilingpoint : Elem -> Maybe Double
  Returns the boiling point (in Kelvin) of an element.

  Totality: total
  Visibility: export
meltingpoint : Elem -> Maybe Double
  Returns the melting point (in Kelvin) of an element.

  Totality: total
  Visibility: export
record IsotopeData : Type
  Additional data about the elements

  Totality: total
  Visibility: public export
  Constructor: 
ID : MassNr -> MolarMass -> Abundance -> IsotopeData

  Projections:
  
.exactMass : IsotopeData -> MolarMass
  
.massNr : IsotopeData -> MassNr
  
.naturalAbundance : IsotopeData -> Abundance

  Hints:
  
Eq IsotopeData
  
Show IsotopeData
.massNr : IsotopeData -> MassNr
  Totality: total
  Visibility: public export
massNr : IsotopeData -> MassNr
  Totality: total
  Visibility: public export
.exactMass : IsotopeData -> MolarMass
  Totality: total
  Visibility: public export
exactMass : IsotopeData -> MolarMass
  Totality: total
  Visibility: public export
.naturalAbundance : IsotopeData -> Abundance
  Totality: total
  Visibility: public export
naturalAbundance : IsotopeData -> Abundance
  Totality: total
  Visibility: public export
arrIsotopeData : IArray 118 (List IsotopeData)
  Totality: total
  Visibility: export
isotopes : Elem -> List IsotopeData
  Get the list of known isotopes for the given element.

  Totality: total
  Visibility: export
isotopeData : Elem -> MassNr -> Maybe IsotopeData
  Get additional information about an element.

  Totality: total
  Visibility: export
naturalMasses : IArray 118 MolarMass
  An array of natural masses of the elements, defined as the average
  of the exact mass of each isotope weighted by natural abundance.

  Totality: total
  Visibility: export
naturalMass : Elem -> MolarMass
  Totality: total
  Visibility: export