diff options
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | thesis.lagda | 13 |
2 files changed, 7 insertions, 7 deletions
@@ -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)) |