Idris2Doc : Text.Smiles.Types

Text.Smiles.Types

(source)
Definitions
record TBIx : Type
  Index for tetrahedral chirality flags as given in the
  OpenSMILES specification

  Totality: total
  Visibility: public export
  Constructor: 
MkTBIx : (value : Bits8) -> {auto 0 _ : FromTo 1 20 value} -> TBIx

  Projections:
  
0 .prf : ({rec:0} : TBIx) -> FromTo 1 20 (value {rec:0})
  
.value : TBIx -> Bits8

  Hints:
  
Eq TBIx
  
Finite TBIx
  
Interpolation TBIx
  
Ord TBIx
  
Show TBIx
.value : TBIx -> Bits8
  Totality: total
  Visibility: public export
value : TBIx -> Bits8
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : TBIx) -> FromTo 1 20 (value {rec:0})
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : TBIx) -> FromTo 1 20 (value {rec:0})
  Totality: total
  Visibility: public export
record OHIx : Type
  Index for octahedral chirality flags as given in the
  OpenSMILES specification

  Totality: total
  Visibility: public export
  Constructor: 
MkOHIx : (value : Bits8) -> {auto 0 _ : FromTo 1 20 value} -> OHIx

  Projections:
  
0 .prf : ({rec:0} : OHIx) -> FromTo 1 20 (value {rec:0})
  
.value : OHIx -> Bits8

  Hints:
  
Eq OHIx
  
Finite OHIx
  
Interpolation OHIx
  
Ord OHIx
  
Show OHIx
.value : OHIx -> Bits8
  Totality: total
  Visibility: public export
value : OHIx -> Bits8
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : OHIx) -> FromTo 1 20 (value {rec:0})
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : OHIx) -> FromTo 1 20 (value {rec:0})
  Totality: total
  Visibility: public export
data Chirality : Type
  Chirality flag of a bracket atom

  Totality: total
  Visibility: public export
  Constructors:
  
None : Chirality
  
CW : Chirality
  
CCW : Chirality
  
TH1 : Chirality
  
TH2 : Chirality
  
AL1 : Chirality
  
AL2 : Chirality
  
SP1 : Chirality
  
SP2 : Chirality
  
SP3 : Chirality
  
TB : TBIx -> Chirality
  
OH : OHIx -> Chirality

  Hints:
  
Eq Chirality
  
Finite Chirality
  
Interpolation Chirality
  
Ord Chirality
  
Show Chirality
data ValidSubset : Elem -> Bool -> Type
  Proof that an element (plus aromaticity flag) is a valid subset
  element that can appear without being wrapped in a pair of
  brackets.

  Totality: total
  Visibility: public export
  Constructors:
  
VB : ValidSubset B b
  
VC : ValidSubset C b
  
VN : ValidSubset N b
  
VO : ValidSubset O b
  
VF : ValidSubset F False
  
VP : ValidSubset P b
  
VS : ValidSubset S b
  
VCl : ValidSubset Cl False
  
VBr : ValidSubset Br False
  
VI : ValidSubset I False

  Hint: 
ValidSubset e b => ValidAromatic e b
0 toValidArom : ValidSubset e b => ValidAromatic e b
  Totality: total
  Visibility: export
data SmilesAtom : Type
  Totality: total
  Visibility: public export
  Constructors:
  
SubsetAtom : (elem : Elem) -> (arom : Bool) -> {auto 0 _ : ValidSubset elem arom} -> SmilesAtom
  
Bracket : Atom AromIsotope Charge () () HCount () Chirality () -> SmilesAtom

  Hints:
  
Cast SmilesAtom Elem
  
Cast SmilesAtom Isotope
  
Cast SmilesAtom AromIsotope
  
Cast SmilesAtom AromElem
  
Eq SmilesAtom
  
Interpolation SmilesAtom
  
Show SmilesAtom
subset : List SmilesAtom
  Totality: total
  Visibility: export
bracket : AromIsotope -> Chirality -> HCount -> Charge -> SmilesAtom
  Totality: total
  Visibility: export
isArom : SmilesAtom -> Bool
  Totality: total
  Visibility: export
encodeCharge : Charge -> String
  Totality: total
  Visibility: export
encodeH : HCount -> String
  Totality: total
  Visibility: export
encodeAtom : SmilesAtom -> String
  Totality: total
  Visibility: export
aromIsotope : Maybe MassNr -> AromElem -> AromIsotope
  Totality: total
  Visibility: export
record RingNr : Type
  An natural number in the range [0,99] representing a ring opening
  or -closure in a SMILES string

  Totality: total
  Visibility: public export
  Constructor: 
MkRingNr : (value : Bits8) -> (0 _ : value <= 99) -> RingNr

  Projections:
  
0 .prf : ({rec:0} : RingNr) -> value {rec:0} <= 99
  
.value : RingNr -> Bits8

  Hints:
  
Eq RingNr
  
Finite RingNr
  
Interpolation RingNr
  
Ord RingNr
  
Show RingNr
.value : RingNr -> Bits8
  Totality: total
  Visibility: public export
value : RingNr -> Bits8
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : RingNr) -> value {rec:0} <= 99
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : RingNr) -> value {rec:0} <= 99
  Totality: total
  Visibility: public export
data SmilesBond : Type
  A bond in a SMILES string

  Totality: total
  Visibility: public export
  Constructors:
  
Sngl : SmilesBond
  
Arom : SmilesBond
  
Dbl : SmilesBond
  
Trpl : SmilesBond
  
Quad : SmilesBond
  
FW : SmilesBond
  
BW : SmilesBond

  Hints:
  
Cast SmilesBond BondOrder
  
Eq SmilesBond
  
Finite SmilesBond
  
Interpolation SmilesBond
  
Ord SmilesBond
  
Show SmilesBond
record Ring : Type
  Totality: total
  Visibility: public export
  Constructor: 
R : RingNr -> Maybe SmilesBond -> Ring

  Projections:
  
.bond : Ring -> Maybe SmilesBond
  
.ring : Ring -> RingNr

  Hints:
  
Eq Ring
  
Finite Ring
  
Interpolation Ring
  
Show Ring
.ring : Ring -> RingNr
  Totality: total
  Visibility: public export
ring : Ring -> RingNr
  Totality: total
  Visibility: public export
.bond : Ring -> Maybe SmilesBond
  Totality: total
  Visibility: public export
bond : Ring -> Maybe SmilesBond
  Totality: total
  Visibility: public export
0 SmilesGraph : Type
  Totality: total
  Visibility: public export