From e0d09d237969f35e92b707dc09779585327ddb52 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 6 Jan 2025 14:03:57 -0500 Subject: [PATCH] Add set length to Util --- src/Util.md | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) 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 +```