@@ -0,0 +1,33 @@
1+module NonLayout
2+
3+{-
4+Haskell and Idris use indentation for grouping in the concrete syntax.
5+How this works is defined as an automatic translation to the equivalent
6+syntax using { ; and }, which you are free to use yourself.
7+
8+In Idris specifically, if let or where is followed by { then indentation no
9+longer matters for the following definitions until a balanced } appears. To
10+put multiple declarations on one line within the { } you put semicolons between
11+them: one ; for let declarations and ;; for where declarations. Whether this
12+discrepancy is a bug I don't know.
13+-}
14+
15+average : String -> Double
16+average str = answer where
17+ wordCount : String -> Nat
18+ wordCount str = length (words str)
19+ wordLengths : List String -> List Nat
20+ wordLengths strs = map length strs
21+ answer =
22+ let numWords = wordCount str in
23+ let totalLength = sum (wordLengths (words str)) in
24+ cast totalLength / cast numWords
25+
26+average' : String -> Double
27+average' str = answer where {
28+ wordCount : String -> Nat ;; wordCount str = length (words str)
29+ wordLengths : List String -> List Nat ;; wordLengths strs = map length strs
30+ answer = let {
31+ numWords = wordCount str; totalLength = sum (wordLengths (words str))
32+ } in cast totalLength / cast numWords
33+}