From: Francesco Mazzoli <f@mazzo.li>
Date: Wed, 22 May 2013 11:51:55 +0000 (+0100)
Subject: hide module declaration
X-Git-Url: https://git.enpas.org/?p=bitonic-mengthesis.git;a=commitdiff_plain;h=5bbbffc580f28704da849395f8fc722e01cc1c45

hide module declaration
---

diff --git a/Makefile b/Makefile
index ad3f550..a5e8cc6 100644
--- a/Makefile
+++ b/Makefile
@@ -33,4 +33,3 @@ clean: cleanup
 
 cleanup:
 	rm -f *.log *.aux *.nav *.snm *.toc *.vrb *.out *.bbl *.blg *.agdai
-
diff --git a/thesis.lagda b/thesis.lagda
index 985c611..4407487 100644
--- a/thesis.lagda
+++ b/thesis.lagda
@@ -15,6 +15,7 @@
 \usepackage[conor]{agda}
 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
+\renewcommand{\AgdaField}{\AgdaFunction}
 \definecolor{AgdaBound} {HTML}{000000}
 
 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
@@ -39,12 +40,12 @@
 
 \begin{document}
 
-%if False
+\iffalse
 \begin{code}
 module thesis where
 open import Level
 \end{code}
-%endif
+\fi
 
 \maketitle
 
@@ -98,7 +99,7 @@ different things:
   \begin{tabular}{c | l}
     $\mytyc{Sans}$  & Type constructors. \\
     $\myind{sans}$  & Data constructors. \\
-    $\myfld{sans}$  & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
+    % $\myfld{sans}$  & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
     $\mysyn{roman}$ & Syntax of the language. \\
     $\myfun{roman}$ & Defined values. \\
     $\myb{math}$    & Bound variables.
@@ -123,12 +124,12 @@ module ITT where
     field
       fst : A
       snd : B fst
-  open _×_ public
 
   data Bool : Set where
     true false : Bool
 
-  if_/_then_else_ : ∀ {a} (x : Bool) → (P : Bool → Set a) → P true → P false → P x
+  if_/_then_else_ : ∀ {a}
+    (x : Bool) → (P : Bool → Set a) → P true → P false → P x
   if true / _ then x else _ = x
   if false / _ then _ else x = x
 
@@ -140,7 +141,7 @@ module ITT where
     ((s : S) →               -- given a shape...
      (f : P s → W S P) →     -- ...and a bunch of kids...
      ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
-     C (_◁_ s f)) →          -- ...does C hold for the node?
+     C (s ◁ f)) →            -- ...does C hold for the node?
     (x : W S P) →            -- If so, ...
     C x                      -- ...C always holds.
   rec C c (s ◁ f) = c s f (λ p → rec C c (f p))