Add set length to Util

This commit is contained in:
Nathan McCarty 2025-01-06 14:03:57 -05:00
parent 061c733688
commit e0d09d2379

View file

@ -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`
<!-- idris
namespace Set
-->
### 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
```