mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-30 15:13:37 +03:00
11 lines
210 B
Idris
11 lines
210 B
Idris
import Data.List
|
|
|
|
[myord] Ord Nat where
|
|
compare Z (S n) = GT
|
|
compare (S n) Z = LT
|
|
compare Z Z = EQ
|
|
compare (S x) (S y) = compare @{myord} x y
|
|
|
|
testList : List Nat
|
|
testList = [3,4,1]
|