Идрис 02

Double

    sqrt : Double -> Double
    exp  : Double -> Double
    log  : Double -> Double

    ceiling : Double -> Double
    floor   : Double -> Double

    euler : Double
    pi    : Double

    cos : Double -> Double
    sin : Double -> Double
    tan : Double -> Double

    acos : Double -> Double
    asin : Double -> Double
    atan : Double -> Double

    cosh : Double -> Double
    sinh : Double -> Double
    tanh : Double -> Double

Char

     chr : Int -> Char
     ord : Char -> Int

     isAlpha : Char -> Bool
     isAlphaNum : Char -> Bool

     isDigit : Char -> Bool
     isHexDigit : Char -> Bool
     isOctDigit : Char -> Bool

     isNL : Char -> Bool             -- ?новая_строка

     isSpace : Char -> Bool

     isUpper : Char -> Bool
     isLower : Char -> Bool

     toLower : Char -> Char
     toUpper : Char -> Char

String

    (++) : String -> String -> String
    length : String -> Nat

    reverse : String -> String
    toLower : String -> String
    toUpper : String -> String

    isInfixOf : String -> String -> Bool
    isPrefixOf : String -> String -> Bool
    isSuffixOf : String -> String -> Bool

    substr : Nat -> Nat -> String -> String
    break : (Char -> Bool) -> String -> (String , String)
    span : (Char -> Bool) -> String -> (String, String)
    split : (Char -> Bool) -> String -> List String

    lines : String -> List String
    unlines : List String -> String
    words : String -> List String
    unwords : List String -> String

    trim : String -> String             -- удаляет пробелы слева и справа
    ltrim : String -> String            -- удаляет пробелы слева

    strCons : Char -> String -> String
    strHead : String -> Char
    strTail : String -> String
    strIndex : String -> Int -> Char

    pack : Foldable t => t Char -> String
    unpack : String -> List Char

List

   lookup : Eq a => a -> List (a , b) -> Maybe b
   head : List a -> a
   init : List a -> List a
   last : List a -> a
   
   drop : Nat -> List a -> List a
   take : Nat -> List a -> List a
   dropWhile : (a -> Bool) -> List a -> List a
   takeWhile : (a -> Bool) -> List a -> List a

   elem : Eq a => a -> List a -> Bool
   filter : (a -> Bool) -> List a -> List a
   find : (a -> Bool) -> List a -> Maybe a
   hasAny : Eq a => List a -> List a -> Bool

   isNil : List a -> Bool
   length : List a -> Nat

   merge : Ord a => List a -> List a -> List a
   sort : Ord a => List a -> List a
   sortBy : (a -> a -> Ordering) -> List a -> List a
   sorted : Ord a => List a -> Bool

   replicate : Nat -> a -> List a
   reverse : List a -> List a
   span : (a -> Bool) -> List a -> (List a, List a)
   toList : Foldable t => t a -> List a
   union : Eq a => List a -> List a -> List a
   unionBy : (a -> a -> Bool) -> List a -> List a -> List a


   map : (a -> b) -> List a -> List b

Stream

   cycle : (xs : List a) -> {auto ok : NonEmpty xs} -> Stream a
   repeat : a -> Stream a

   head : Stream a -> a
   tail : Stream a -> Stream a
   take : Nat -> Stream a -> List a
   drop : Nat -> Stream a -> Stream a

   iterate : (a -> a) -> a -> Stream a
   scanl : (a -> b -> a) -> a -> Stream b -> Stream a

   zip : Stream a -> Stream b -> Stream (a, b)
   unzip : Stream (a, b) -> (Stream a, Stream b)
   zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c

   map  : (a -> b) -> Stream a -> Stream b

Data.Vect

   lookup : Eq a => a -> Vect n (a , b) -> Maybe b 
   lookupBy : (a -> a -> Bool) -> a -> Vect n (a, b) -> Maybe b

   take : (n : Nat) -> Vect (n + m) a -> Vect n a
   takeWhile : (a -> Bool) -> Vect n a -> (q : Nat ** Vect q a)
   drop : (n : Nat) -> Vect (n + m) a -> Vect m a
   dropWhile : (a -> Bool) -> Vect n a -> (q : Nat ** Vect q a)

   head : Vect n a -> a
   tail : Vect (S n) a -> Vect n a
   init : Vect (S n) a -> Vect n a
   last : Vect (S n) a -> a
   index : Fin n -> Vect n a -> a

   Elem : a -> Vect k a -> Type
   Here : Elem x (x :: xs)
   There : Elem x xs -> Elem x (y :: xs)
   find : (a -> Bool) -> Vect n a -> Maybe a

   delete : Eq a => a -> Vect n a -> (p : Nat ** Vect p a)
   deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
   deleteBy : (a -> a -> Bool) -> a -> Vect n a -> (p : Nat ** Vect p a)

   elem : Eq a => a -> Vect n a -> Bool
   elemBy : (a -> a -> Bool) -> a -> Vect n a -> Bool

   filter : (a -> Bool) -> Vect n a -> (p : Nat ** Vect p a)
   foldl1 : (t -> t -> t) -> Vect (S n) t -> t
   foldr1 : (t -> t -> t) -> Vect (S n) t -> t
   
   fromList : (l : List a) -> Vect (length l) a
   fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a

   hasAny : Eq a => Vect m a -> Vect n a -> Bool
   hasAnyBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool

   replicate : (n : Nat) -> a -> Vect n a
   merge : Ord a => Vect n a -> Vect m a -> Vect (n + m) a
   mergeBy : (a -> a -> Ordering) -> Vect n a -> Vect m a -> Vect (n + m) a
   reverse : Vect n a -> Vect n a
   partition : (a -> Bool) -> Vect n a -> ((p : Nat ** Vect p a), (q : Nat ** Vect q a))

   nub : Eq a => Vect n a -> (p : Nat ** Vect p a)
   nubBy : (a -> a -> Bool) -> Vect n a -> (p : Nat ** Vect p a)

   replaceAt : Fin n -> t -> Vect n t -> Vect n t
   replaceByElem : (xs : Vect k t) -> Elem x xs -> t -> Vect k t
   replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)

   scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b

   splitAt : (n : Nat) -> Vect (n + m) a -> (Vect n a, Vect m a)
   updateAt : Fin n -> (t -> t) -> Vect n t -> Vect n t
   
   zip : Vect n a -> Vect n b -> Vect n (a, b)
   unzip : Vect n (a, b) -> (Vect n a, Vect n b)
   zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c