Написал двухстрочник isSorted (одна строчка — тип, вторая — значение (реализация функции))
@
не затайпчекался

бля прикол

% cat << EOF > hello.idr
heredoc> main : IO ()
heredoc> main = putStrLn "Hello world"
heredoc> EOF

% idris hello.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.11.2
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help                

Type checking ./hello.idr
*hello> :compile hello.native
*hello> :js hello.js
*hello> 
Bye bye

% ./hello.native 
Hello world

% ls -l hello*
-rwxrwxr-x 1 ulidtko ulidtko 110K чер 19 02:15 hello*
-rw-rw-r-- 1 ulidtko ulidtko  240 чер 19 02:17 hello.ibc
-rw-rw-r-- 1 ulidtko ulidtko   43 чер 19 02:17 hello.idr
-rw-rw-r-- 1 ulidtko ulidtko  36K чер 19 02:18 hello.js
-rwxrwxr-x 1 ulidtko ulidtko 110K чер 19 02:18 hello.native*

110K
36K

-- на самом деле будущее.

3.9 so
The so data type is a predicate on Bool which guarantees that the value is true:

data so : Bool -> Type where
    oh : so True

This is most useful for providing a static guarantee that a dynamic check has been made. For example, we
might provide a safe interface to a function which draws a pixel on a graphical display as follows, where
so (inBounds x y) guarantees that the point (x,y) is within the bounds of a 640 × 480 window:

inBounds : Int -> Int -> Bool
inBounds x y = x >= 0 && x < 640 && y >= 0 && y < 480
drawPoint : (x : Int) -> (y : Int) -> so (inBounds x y) -> IO ()
drawPoint x y p = unsafeDrawPoint x y

ле к