Idris2Doc : Chem.Types

Chem.Types

(source)
Reexports
import public Data.List.Quantifiers.Extra
import public Data.Refined
import public Data.Refined.Bits16
import public Data.Refined.Bits8
import public Data.Refined.Int8
Definitions
0 IsAtomicNr : Bits8 -> Type
  Proof that a number is in the range [1,118]

  Totality: total
  Visibility: public export
record AtomicNr : Type
  A refined integer in the range [1,118]

  Totality: total
  Visibility: public export
  Constructor: 
MkAtomicNr : (value : Bits8) -> {auto 0 _ : IsAtomicNr value} -> AtomicNr

  Projections:
  
0 .prf : ({rec:0} : AtomicNr) -> IsAtomicNr (value {rec:0})
  
.value : AtomicNr -> Bits8

  Hints:
  
Eq AtomicNr
  
Ord AtomicNr
  
Show AtomicNr
.value : AtomicNr -> Bits8
  Totality: total
  Visibility: public export
value : AtomicNr -> Bits8
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : AtomicNr) -> IsAtomicNr (value {rec:0})
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : AtomicNr) -> IsAtomicNr (value {rec:0})
  Totality: total
  Visibility: public export
record MassNr : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkMassNr : (value : Bits16) -> {auto 0 _ : FromTo 1 511 value} -> MassNr

  Projections:
  
0 .prf : ({rec:0} : MassNr) -> FromTo 1 511 (value {rec:0})
  
.value : MassNr -> Bits16

  Hints:
  
Eq MassNr
  
Interpolation MassNr
  
Ord MassNr
  
Show MassNr
.value : MassNr -> Bits16
  Totality: total
  Visibility: public export
value : MassNr -> Bits16
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : MassNr) -> FromTo 1 511 (value {rec:0})
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : MassNr) -> FromTo 1 511 (value {rec:0})
  Totality: total
  Visibility: public export
MinAbundanceValue : Double
  Totality: total
  Visibility: public export
IsAbundance : Double -> Bool
  Totality: total
  Visibility: public export
record Abundance : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkAbundance : (value : Double) -> {auto 0 _ : Holds IsAbundance value} -> Abundance

  Projections:
  
0 .prf : ({rec:0} : Abundance) -> Holds IsAbundance (value {rec:0})
  
.value : Abundance -> Double

  Hints:
  
Eq Abundance
  
Interpolation Abundance
  
Monoid Abundance
  
Ord Abundance
  
Semigroup Abundance
  
Show Abundance
.value : Abundance -> Double
  Totality: total
  Visibility: public export
value : Abundance -> Double
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : Abundance) -> Holds IsAbundance (value {rec:0})
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : Abundance) -> Holds IsAbundance (value {rec:0})
  Totality: total
  Visibility: public export
multAbundance : Abundance -> Abundance -> Abundance
  Totality: total
  Visibility: public export
MaxMolecularMass : Double
  Molecular mass in g/mol
  
  The total mass of ordinary matter of the universe is assumed to be
  approximately 1.5 * 10^50 kg, so we probably shouldn't exceed that by too
  much.

  Totality: total
  Visibility: public export
IsMolecularMass : Double -> Bool
  Totality: total
  Visibility: public export
record MolecularMass : Type
  Molecular mass (or molecular weight) in g/mol

  Totality: total
  Visibility: public export
  Constructor: 
MkMolecularMass : (value : Double) -> {auto 0 _ : Holds IsMolecularMass value} -> MolecularMass

  Projections:
  
0 .prf : ({rec:0} : MolecularMass) -> Holds IsMolecularMass (value {rec:0})
  
.value : MolecularMass -> Double

  Hints:
  
Cast MolecularMass MolarMass
  
Cast MolarMass MolecularMass
  
Eq MolecularMass
  
Interpolation MolecularMass
  
Monoid MolecularMass
  
Ord MolecularMass
  
Semigroup MolecularMass
  
Show MolecularMass
.value : MolecularMass -> Double
  Totality: total
  Visibility: public export
value : MolecularMass -> Double
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : MolecularMass) -> Holds IsMolecularMass (value {rec:0})
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : MolecularMass) -> Holds IsMolecularMass (value {rec:0})
  Totality: total
  Visibility: public export
addMolecularMass : MolecularMass -> MolecularMass -> MolecularMass
  Totality: total
  Visibility: public export
multMolecularMass : Nat -> MolecularMass -> MolecularMass
  Totality: total
  Visibility: public export
record MolarMass : Type
  Molar mass in Da

  Totality: total
  Visibility: public export
  Constructor: 
MkMolarMass : (value : Double) -> {auto 0 _ : Holds IsMolecularMass value} -> MolarMass

  Projections:
  
0 .prf : ({rec:0} : MolarMass) -> Holds IsMolecularMass (value {rec:0})
  
.value : MolarMass -> Double

  Hints:
  
Cast MolecularMass MolarMass
  
Cast MolarMass MolecularMass
  
Eq MolarMass
  
Interpolation MolarMass
  
Monoid MolarMass
  
Ord MolarMass
  
Semigroup MolarMass
  
Show MolarMass
.value : MolarMass -> Double
  Totality: total
  Visibility: public export
value : MolarMass -> Double
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : MolarMass) -> Holds IsMolecularMass (value {rec:0})
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : MolarMass) -> Holds IsMolecularMass (value {rec:0})
  Totality: total
  Visibility: public export
molarMass : Double -> MolarMass
  Totality: total
  Visibility: export
addMolarMass : MolarMass -> MolarMass -> MolarMass
  Totality: total
  Visibility: export
interface HasMolarMass : Type -> Type
  Parameters: a
Methods:
  
mass : a -> MolarMass
  Extract the molecular mass of an element or isotope.
  In case of an element, this returns the average molar mass
  in case of an isotope, it's the same as `exactMass`.
  
exactMass : a -> MolarMass
  Extract the exact molecular mass of an element or isotope.
  In case of an `Elem`, this returns the exact mass of the most
  abundant isotope.

Implementations:
  
HasMolarMass Elem
  
HasMolarMass Isotope
  
HasMolarMass AromIsotope
mass : HasMolarMass a => a -> MolarMass
  Extract the molecular mass of an element or isotope.
  In case of an element, this returns the average molar mass
  in case of an isotope, it's the same as `exactMass`.

  Totality: total
  Visibility: public export
exactMass : HasMolarMass a => a -> MolarMass
  Extract the exact molecular mass of an element or isotope.
  In case of an `Elem`, this returns the exact mass of the most
  abundant isotope.

  Totality: total
  Visibility: public export
multByAbundance : Abundance -> MolarMass -> MolarMass
  Totality: total
  Visibility: export
record Charge : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCharge : (value : Int8) -> {auto 0 _ : FromTo -15 15 value} -> Charge

  Projections:
  
0 .prf : ({rec:0} : Charge) -> FromTo -15 15 (value {rec:0})
  
.value : Charge -> Int8

  Hints:
  
Eq Charge
  
Finite Charge
  
Interpolation Charge
  
Ord Charge
  
Show Charge
.value : Charge -> Int8
  Totality: total
  Visibility: public export
value : Charge -> Int8
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : Charge) -> FromTo -15 15 (value {rec:0})
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : Charge) -> FromTo -15 15 (value {rec:0})
  Totality: total
  Visibility: public export
incCharge : Charge -> Charge
  Increase a charge value by one.
  
  Returns the unmodified input if it is already the maximal valid value.

  Totality: total
  Visibility: export
decCharge : Charge -> Charge
  Decrease a charge value by one.
  
  Returns the unmodified input if it is already the minimal valid value.

  Totality: total
  Visibility: export
record HCount : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkHCount : (value : Bits8) -> {auto 0 _ : value < 10} -> HCount

  Projections:
  
0 .prf : ({rec:0} : HCount) -> value {rec:0} < 10
  
.value : HCount -> Bits8

  Hints:
  
Cast e Elem => Cast (Atom e c p r HCount t ch l) Formula
  
Eq HCount
  
Finite HCount
  
HasMolecularMass HCount
  
Interpolation HCount
  
Ord HCount
  
Show HCount
.value : HCount -> Bits8
  Totality: total
  Visibility: public export
value : HCount -> Bits8
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : HCount) -> value {rec:0} < 10
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : HCount) -> value {rec:0} < 10
  Totality: total
  Visibility: public export
data NoH : Type
  Placeholder for atoms without implicit hydrogens.
  
  We can use this instead of `Unit` (`()`), to signal that an atom
  does not have any implicit hydrogens, as oppsed to the implicit
  H-count not having been determined yet.
  
  For instance, we can have an implementation of
  `Cast (Atom Elem c p r NoH t ch l) Formula`, because here we
  do not have to add any implicit hydrogens to such an atom,
  while no such implementation should be written for
  `Cast (Atom Elem c p r () t ch l) Formula`, because in this case,
  the `Unit` tag implies that implicit hydrogens have not been
  determined yet.

  Totality: total
  Visibility: public export
  Constructor: 
HasNoH : NoH

  Hints:
  
Cast e Elem => Cast (Atom e c p r NoH t ch l) Formula
  
Eq NoH
  
HasMolecularMass NoH
  
Ord NoH
  
Show NoH
data Radical : Type
  Type of radical if any.

  Totality: total
  Visibility: public export
  Constructors:
  
NoRadical : Radical
  
Singlet : Radical
  
Doublet : Radical
  
Triplet : Radical

  Hints:
  
Eq Radical
  
Finite Radical
  
Ord Radical
  
Show Radical
data Hybridization : Type
  Kinds of hybridization

  Totality: total
  Visibility: public export
  Constructors:
  
None : Hybridization
  
Planar : Hybridization
  
S : Hybridization
  
SP : Hybridization
  
SP2 : Hybridization
  
SP3 : Hybridization
  
SP3D1 : Hybridization
  
SP3D2 : Hybridization
  
Tetrahedral : Hybridization
  
Octahedral : Hybridization

  Hints:
  
Cast SmilesAtomAT Hybridization
  
Eq Hybridization
  
Finite Hybridization
  
Ord Hybridization
  
Show Hybridization
data BondOrder : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Single : BondOrder
  
Dbl : BondOrder
  
Triple : BondOrder

  Hints:
  
Cast SmilesBond BondOrder
  
Cast MolBond BondOrder
  
Cast BondOrder MolBond
  
Cast a BondOrder => Cast (AromBond a) BondOrder
  
Eq BondOrder
  
Interpolation BondOrder
  
Ord BondOrder
  
Show BondOrder
0 ChemRes : List Type -> Type -> Type
  Totality: total
  Visibility: public export