Idris2Doc : Chem.Isotope

Chem.Isotope

(source)
Definitions
record Isotope : Type
  An element paired with an optional mass number.
  
  If the mass number is `Nothing`, a value of this type represents
  a natural mixture of isotopes.

  Totality: total
  Visibility: public export
  Constructor: 
MkI : Elem -> Maybe MassNr -> Isotope

  Projections:
  
.elem : Isotope -> Elem
  
.mass : Isotope -> Maybe MassNr

  Hints:
  
Cast Isotope Elem
  
Cast Elem Isotope
  
Cast Isotope AromElem
  
Cast AromElem Isotope
  
Cast AromIsotope Isotope
  
Cast Isotope AromIsotope
  
Eq Isotope
  
HasMolarMass Isotope
  
Show Isotope
.elem : Isotope -> Elem
  Totality: total
  Visibility: public export
elem : Isotope -> Elem
  Totality: total
  Visibility: public export
.mass : Isotope -> Maybe MassNr
  Totality: total
  Visibility: public export
mass : Isotope -> Maybe MassNr
  Totality: total
  Visibility: public export
record AromIsotope : Type
  An element paired with an optional mass number plus a
  boolean flag representing aromaticity.
  
  If the mass number is `Nothing`, a value of this type represents
  a natural mixture of isotopes.

  Totality: total
  Visibility: public export
  Constructor: 
MkAI : (elem : Elem) -> Maybe MassNr -> (arom : Bool) -> {auto 0 _ : ValidAromatic elem arom} -> AromIsotope

  Projections:
  
.arom : AromIsotope -> Bool
  
.elem : AromIsotope -> Elem
  
.mass : AromIsotope -> Maybe MassNr
  
0 .prf : ({rec:0} : AromIsotope) -> ValidAromatic (elem {rec:0}) (arom {rec:0})

  Hints:
  
Cast AromIsotope Elem
  
Cast Elem AromIsotope
  
Cast AromIsotope AromElem
  
Cast AromElem AromIsotope
  
Cast AromIsotope Isotope
  
Cast Isotope AromIsotope
  
Eq AromIsotope
  
HasMolarMass AromIsotope
  
Show AromIsotope
.elem : AromIsotope -> Elem
  Totality: total
  Visibility: public export
elem : AromIsotope -> Elem
  Totality: total
  Visibility: public export
.mass : AromIsotope -> Maybe MassNr
  Totality: total
  Visibility: public export
mass : AromIsotope -> Maybe MassNr
  Totality: total
  Visibility: public export
.arom : AromIsotope -> Bool
  Totality: total
  Visibility: public export
arom : AromIsotope -> Bool
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : AromIsotope) -> ValidAromatic (elem {rec:0}) (arom {rec:0})
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : AromIsotope) -> ValidAromatic (elem {rec:0}) (arom {rec:0})
  Totality: total
  Visibility: public export