Idris2Doc : CyBy.Draw.Internal.CoreDims

CyBy.Draw.Internal.CoreDims

(source)
Definitions
record CoreDims : Type
  Core drawing settings used for computing the geometric properties of
  drawn molecules.

  Totality: total
  Visibility: public export
  Constructor: 
CD : Double -> Double -> Double -> Double -> (angleSteps : Nat) -> String -> Nat -> Nat -> Double -> Double -> Double -> Double -> Double -> Measure -> (0 _ : IsSucc angleSteps) -> CoreDims

  Projections:
  
.angleSteps : CoreDims -> Nat
  
.bondBGWidth : CoreDims -> Double
  
.bondWidth : CoreDims -> Double
  
.downWedgeGap : CoreDims -> Double
  Gap between two bars of a downward facing wedge
  
.font : CoreDims -> String
  
.fontSize : CoreDims -> Nat
  
.halfWaveLength : CoreDims -> Double
  Half the wavelength of a wavy bond
  
.measure : CoreDims -> Measure
  Utility used for measuring text
  
.radiusAtom : CoreDims -> Double
  
.selectBufferSize : CoreDims -> Double
  
0 .stepsPrf : ({rec:0} : CoreDims) -> IsSucc (angleSteps {rec:0})
  
.subscriptSize : CoreDims -> Nat
  
.waveAmplitude : CoreDims -> Double
  Amplitude of a wavy bond
  
.wedgeNarrowEnd : CoreDims -> Double
  Width of the narrow end of a wedge
  
.wedgeWideEnd : CoreDims -> Double
  Width of the wide end of a wedge

  Hints:
  
CoreDims => Bounded Label
  
DrawSettings => CoreDims
.radiusAtom : CoreDims -> Double
  Totality: total
  Visibility: public export
radiusAtom : CoreDims -> Double
  Totality: total
  Visibility: public export
.bondWidth : CoreDims -> Double
  Totality: total
  Visibility: public export
bondWidth : CoreDims -> Double
  Totality: total
  Visibility: public export
.bondBGWidth : CoreDims -> Double
  Totality: total
  Visibility: public export
bondBGWidth : CoreDims -> Double
  Totality: total
  Visibility: public export
.selectBufferSize : CoreDims -> Double
  Totality: total
  Visibility: public export
selectBufferSize : CoreDims -> Double
  Totality: total
  Visibility: public export
.angleSteps : CoreDims -> Nat
  Totality: total
  Visibility: public export
angleSteps : CoreDims -> Nat
  Totality: total
  Visibility: public export
.font : CoreDims -> String
  Totality: total
  Visibility: public export
font : CoreDims -> String
  Totality: total
  Visibility: public export
.fontSize : CoreDims -> Nat
  Totality: total
  Visibility: public export
fontSize : CoreDims -> Nat
  Totality: total
  Visibility: public export
.subscriptSize : CoreDims -> Nat
  Totality: total
  Visibility: public export
subscriptSize : CoreDims -> Nat
  Totality: total
  Visibility: public export
.downWedgeGap : CoreDims -> Double
  Gap between two bars of a downward facing wedge

  Totality: total
  Visibility: public export
downWedgeGap : CoreDims -> Double
  Gap between two bars of a downward facing wedge

  Totality: total
  Visibility: public export
.wedgeNarrowEnd : CoreDims -> Double
  Width of the narrow end of a wedge

  Totality: total
  Visibility: public export
wedgeNarrowEnd : CoreDims -> Double
  Width of the narrow end of a wedge

  Totality: total
  Visibility: public export
.wedgeWideEnd : CoreDims -> Double
  Width of the wide end of a wedge

  Totality: total
  Visibility: public export
wedgeWideEnd : CoreDims -> Double
  Width of the wide end of a wedge

  Totality: total
  Visibility: public export
.halfWaveLength : CoreDims -> Double
  Half the wavelength of a wavy bond

  Totality: total
  Visibility: public export
halfWaveLength : CoreDims -> Double
  Half the wavelength of a wavy bond

  Totality: total
  Visibility: public export
.waveAmplitude : CoreDims -> Double
  Amplitude of a wavy bond

  Totality: total
  Visibility: public export
waveAmplitude : CoreDims -> Double
  Amplitude of a wavy bond

  Totality: total
  Visibility: public export
.measure : CoreDims -> Measure
  Utility used for measuring text

  Totality: total
  Visibility: public export
measure : CoreDims -> Measure
  Utility used for measuring text

  Totality: total
  Visibility: public export
0 .stepsPrf : ({rec:0} : CoreDims) -> IsSucc (angleSteps {rec:0})
  Totality: total
  Visibility: public export
0 stepsPrf : ({rec:0} : CoreDims) -> IsSucc (angleSteps {rec:0})
  Totality: total
  Visibility: public export
defaultCore : CoreDims
  Totality: total
  Visibility: export