small fix to Assignment 4
This commit is contained in:
parent
20ae9af4f6
commit
649d7dcb13
2 changed files with 4 additions and 1 deletions
|
@ -33,6 +33,9 @@ agda = count (prefix begin) (prefix end) . lines
|
||||||
begin = "\\begin{code}"
|
begin = "\\begin{code}"
|
||||||
end = "\\end{code}"
|
end = "\\end{code}"
|
||||||
|
|
||||||
|
nonblank :: String -> Bool
|
||||||
|
nonblank = not . all (== ' ')
|
||||||
|
|
||||||
wc :: String -> Int
|
wc :: String -> Int
|
||||||
wc = length . lines
|
wc = length . lines
|
||||||
|
|
||||||
|
|
|
@ -52,7 +52,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||||
|
|
||||||
|
|
||||||
\begin{code}
|
\begin{code}
|
||||||
module More where
|
module DeBruijn where
|
||||||
\end{code}
|
\end{code}
|
||||||
|
|
||||||
Remember to indent all code by two spaces.
|
Remember to indent all code by two spaces.
|
||||||
|
|
Loading…
Reference in a new issue