X-Git-Url: https://git.enpas.org/?a=blobdiff_plain;f=thesis.lagda;h=4407487576d51c940dfba9fd9af1020d814001b2;hb=5bbbffc580f28704da849395f8fc722e01cc1c45;hp=985c611168e1c77aefb4fd8672a6f8784c6afbb0;hpb=a0e46e3bf7b0f6b439681e7b62a63d4bd682f4e4;p=bitonic-mengthesis.git

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))