diff --git a/src/Util.md b/src/Util.md index c551eea..f015e61 100644 --- a/src/Util.md +++ b/src/Util.md @@ -4,6 +4,10 @@ This module contains functions that extend the functionality of standard data ty ```idris module Util + +import Data.SortedSet + +%default total ``` ## Either @@ -45,3 +49,20 @@ namespace Pair (x_1, x_2) >-< (y_1, y_2) = (x_1 - y_1, x_2 - y_2) ``` +## Set + +Extend `Data.SortedSet` + + + +### length + +Count the number of elements in a sorted set + +```idris + export + length : SortedSet k -> Nat + length x = foldl (\acc, e => acc + 1) 0 x +```