Idris2Doc : Data.Refined.String

Data.Refined.String

(source)
Reexports
import public Data.Refined.Char
import public Data.Refined.List
import public Data.Refined.Core
Definitions
0 Len : (Integer -> Type) -> String -> Type
  Totality: total
  Visibility: public export
0 Str : (List Char -> Type) -> String -> Type
  Totality: total
  Visibility: public export
data LeftTrimmed : List Char -> Type
  Proof that a (non-empty) list of characters does not start with
  a whitespace character.

  Totality: total
  Visibility: public export
  Constructor: 
LTCons : Holds (not . isControl) c -> LeftTrimmed (c :: cs)

  Hints:
  
HDec (List Char) LeftTrimmed
  
HDec0 (List Char) LeftTrimmed
data RightTrimmed : List Char -> Type
  Proof that a list of characters does not start with a whitespace character.

  Totality: total
  Visibility: public export
  Constructors:
  
RT1 : Holds (not . isControl) c -> RightTrimmed [c]
  
RTCons : RightTrimmed cs -> RightTrimmed (c :: cs)

  Hints:
  
HDec (List Char) RightTrimmed
  
HDec0 (List Char) RightTrimmed
0 Trimmed : List Char -> Type
  Totality: total
  Visibility: public export