Clean up whitespace

Author: yurrriq

Makefile

@@ -1,28 +1,39 @@
 PKG   := software_foundations
+
+
 # TODO: Find idris executable.
 IDRIS ?= idris
 
+
 .PHONY: pdf site
 
+
 all: pdf site
 
+
 build:
 	$(IDRIS) --build $(PKG).ipkg
 
+
 pdf:
 	$(MAKE) -C src
 	mv src/all.pdf docs/pdf/sf-idris-2016.pdf
 
+
 clean-all: clean clean-docs
 
+
 clean:
 	$(IDRIS) --clean $(PKG).ipkg
 
+
 clean-docs:
 	$(MAKE) -C src clean
 	@$(RM) docs/index.html >/dev/null
 
+
 site: docs/index.html
 
+
 docs/index.html: README.md
 	pandoc -f markdown_github -t html -s -o $@ $<

src/Basics.lidr

@@ -61,8 +61,8 @@ that can be used to prove simple properties of Idris programs.
 
 One unusual aspect of Coq is that its set of built-in features is _extremely_
 small, For example, instead of providing the usual palette of atomic data types
-(booleans, integers, strings, etc.), Coq offers a powerful mechanism for 
-defining new data types from scratch, from which all these familiar types arise 
+(booleans, integers, strings, etc.), Coq offers a powerful mechanism for
+defining new data types from scratch, from which all these familiar types arise
 as instances.
 
 Naturally, the Coq distribution comes with an extensive standard library
@@ -229,7 +229,7 @@ members `False` and `True`.
 data Bool = True | False
 ```
 
-This definition is written in the simplified style, similar to `Day`. It can 
+This definition is written in the simplified style, similar to `Day`. It can
 also be written in the verbose style:
 
 ```idris
@@ -238,7 +238,7 @@ data Bool : Type where
     False : Bool
 ```
 
-The verbose style is more powerful because it allows us to assign precise 
+The verbose style is more powerful because it allows us to assign precise
 types to individual constructors. This will become very useful later on.
 
 Although we are rolling our own booleans here for the sake of building up
@@ -282,7 +282,7 @@ truth table -- for the `orb` function:
 -- TODO: Edit this
 
 We can also introduce some familiar syntax for the boolean operations we have
-just defined. The `syntax` command defines a new symbolic notation for an 
+just defined. The `syntax` command defines a new symbolic notation for an
 existing definition, and `infixl` specifies left-associative fixity.
 \color{black}
 
@@ -301,9 +301,9 @@ existing definition, and `infixl` specifies left-associative fixity.
 
 === Exercises: 1 star (nandb)
 
-Fill in the hole `?nandb_rhs` and complete the following function; then make 
-sure that the assertions below can each be verified by Idris. (Fill in each of 
-the holes, following the model of the `orb` tests above.) The function should 
+Fill in the hole `?nandb_rhs` and complete the following function; then make
+sure that the assertions below can each be verified by Idris. (Fill in each of
+the holes, following the model of the `orb` tests above.) The function should
 return `True` if either or both of its inputs are `False`.
 
 >   nandb : (b1 : Bool) -> (b2 : Bool) -> Bool
@@ -395,8 +395,8 @@ Idris provides a _module system_, to aid in organizing large developments.
 > namespace Numbers
 
 The types we have defined so far are examples of "enumerated types": their
-definitions explicitly enumerate a finite set of elements. A More interesting 
-way of defining a type is to give a collection of _inductive rules_ describing 
+definitions explicitly enumerate a finite set of elements. A More interesting
+way of defining a type is to give a collection of _inductive rules_ describing
 its elements. For example, we can define the natural numbers as follows:
 
 ```idris

src/Induction.lidr

@@ -176,14 +176,14 @@ plus_rearrange_firsttry n m p q = rewrite plus_comm in Refl
 ```
 When checking right hand side of plus_rearrange_firsttry with expected type
         n + m + (p + q) = m + n + (p + q)
-                          
+
 _ does not have an equality type ((n1 : Nat) ->
 (n1 : Nat) -> plus n1 m1 = plus m1 n1)
 ```
 
 To get `plus_comm` to apply at the point where we want it to, we can introduce a
-local lemma using the `where` keyword stating that `n + m = m + n` (for the 
-particular `m` and `n` that we are talking about here), prove this lemma using 
+local lemma using the `where` keyword stating that `n + m = m + n` (for the
+particular `m` and `n` that we are talking about here), prove this lemma using
 `plus_comm`, and then use it to do the desired rewrite.
 
 > plus_rearrange : (n, m, p, q : Nat) ->

src/Makefile

@@ -1,32 +1,40 @@
 .DEFAULT_GOAL := all.pdf
 
+
 # TODO: Find pandoc executable.
 PANDOC    ?= pandoc
 
+
 PANDOC_FLAGS := \
 	--filter pandoc-minted.hs --latex-engine=xelatex \
 	-f markdown+lhs+tex_math_single_backslash -t latex+lhs \
 	--top-level-division=chapter
 
+
 LIDRFILES := Preface.lidr \
 	Basics.lidr \
 	Induction.lidr
 # TODO: Add more chapters, in order, here.
 
+
 TEXFILES  := $(LIDRFILES:.lidr=.tex)
 
 
 .PHONY: all clean
 
+
 clean:
 	rm -rf all.{aux,log,out,toc,pdf} _minted-all $(TEXFILES)
 
+
 all.pdf: all.tex
 	latexmk -xelatex -e '$$pdflatex=q/xelatex %O --shell-escape %S/' $<
 
+
 all.tex: book.tex $(TEXFILES)
 	$(PANDOC) $(PANDOC_FLAGS) -N --toc -o $@ \
 	$(foreach texfile,$(TEXFILES),-A $(texfile)) $<
 
+
 %.tex: %.lidr
 	$(PANDOC) $(PANDOC_FLAGS) -o $@ $<