Noratrieb/idris-learning
1
0
Fork 0
mirror of https://github.com/Noratrieb/idris-learning.git synced 2026-01-15 21:45:01 +01:00
Code Issues Projects Releases Packages Wiki Activity Actions

move and change

Browse source
This commit is contained in:
nora 2021-07-08 16:46:51 +02:00
parent 80aa1a2be7
commit 1330cb05e9
10 changed files with 161 additions and 142 deletions
Download patch file Download diff file Expand all files Collapse all files

17
Average.idr
View file

@ -1,17 +0,0 @@
module Average
import Data.String
||| Calculate the average word length of a string
||| @str a string containing words seperated by whitespace
export
average : (str : String) -> Double
average str = let totalLength = sum (wordLengths str)
wordAmount = wordCount str in
cast totalLength / cast wordAmount
where
wordCount : String -> Nat
wordCount str = length (words str)
wordLengths : String -> List Nat
wordLengths str = map length (words str)