projects
/
bitonic-mengthesis.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
a0e46e3
)
hide module declaration
author
Francesco Mazzoli
<f@mazzo.li>
Wed, 22 May 2013 11:51:55 +0000
(12:51 +0100)
committer
Francesco Mazzoli
<f@mazzo.li>
Wed, 22 May 2013 11:51:55 +0000
(12:51 +0100)
Makefile
patch
|
blob
|
history
thesis.lagda
patch
|
blob
|
history
diff --git
a/Makefile
b/Makefile
index ad3f550125f36e7e0baefe060566d280df3cd9ed..a5e8cc68ae0549670fbabfce16724677363d55b7 100644
(file)
--- a/
Makefile
+++ b/
Makefile
@@
-33,4
+33,3
@@
clean: cleanup
cleanup:
rm -f *.log *.aux *.nav *.snm *.toc *.vrb *.out *.bbl *.blg *.agdai
cleanup:
rm -f *.log *.aux *.nav *.snm *.toc *.vrb *.out *.bbl *.blg *.agdai
-
diff --git
a/thesis.lagda
b/thesis.lagda
index 985c611168e1c77aefb4fd8672a6f8784c6afbb0..4407487576d51c940dfba9fd9af1020d814001b2 100644
(file)
--- 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}}}
\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}}
\definecolor{AgdaBound} {HTML}{000000}
\DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
@@
-39,12
+40,12
@@
\begin{document}
\begin{document}
-
%if F
alse
+
\iff
alse
\begin{code}
module thesis where
open import Level
\end{code}
\begin{code}
module thesis where
open import Level
\end{code}
-%endif
+\fi
\maketitle
\maketitle
@@
-98,7
+99,7
@@
different things:
\begin{tabular}{c | l}
$\mytyc{Sans}$ & Type constructors. \\
$\myind{sans}$ & Data constructors. \\
\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.
$\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
field
fst : A
snd : B fst
- open _×_ public
data Bool : Set where
true false : Bool
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
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...
((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))
(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))