Skip to content

Commit

Permalink
Remove empty lines from inside equation blocks
Browse files Browse the repository at this point in the history
Works in VS Code markdown preview, but breaks pandoc conversion.
  • Loading branch information
lukstafi committed Oct 26, 2023
1 parent 9409c48 commit 62dfb7d
Show file tree
Hide file tree
Showing 6 changed files with 52 additions and 52 deletions.
8 changes: 3 additions & 5 deletions chapter1/functional-lecture01.md
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,9 @@ $$ \frac{\frac{\begin{array}{ll}
\small{x}}{\text{go outdoor}}
\end{array}}{\text{nice view}}
\end{array}}{\text{happy}}}{\text{sunny} \rightarrow \text{happy}}
\small{\text{ using } x} $$Elimination rule for disjunction represents **reasoning by cases**.
\small{\text{ using } x} $$

Elimination rule for disjunction represents **reasoning by cases**.

How can we use the fact that it is sunny$\vee$cloudy (but not rainy)?

Expand All @@ -135,7 +137,6 @@ natural numbers:

$$ \frac{\begin{array}{rr}
p (0) &
{{{\frac{\,}{p(x)} \tiny{x}} \atop {\text{\textbar}}} \atop {p(x+1)}}
\end{array}}{p (n)} \text{ by induction, using } x $$

Expand Down Expand Up @@ -225,7 +226,6 @@ than these:

$$ \frac{\begin{array}{ll}
e_{1} : a &
{{{\frac{\,}{x : a} \tiny{x}} \atop {\text{\textbar}}} \atop {e_2 : b}}
\end{array}}{\text{{\texttt{let}} } x \text{{\texttt{=}}}
e_{1} \text{ \text{{\texttt{in}}} } e_{2} : b} $$
Expand All @@ -234,9 +234,7 @@ $$ \frac{\begin{array}{ll}
$\rightarrow$), and:

$$ \frac{\begin{array}{ll}
{{{\frac{\,}{x : a} \tiny{x}} \atop {\text{\textbar}}} \atop {e_1 : a}} &
{{{\frac{\,}{x : a} \tiny{x}} \atop {\text{\textbar}}} \atop {e_2 : b}}
\end{array}}{\text{{\texttt{let rec}} } x
\text{{\texttt{=}}} e_{1} \text{ \text{{\texttt{in}}} } e_{2}
Expand Down
6 changes: 2 additions & 4 deletions chapter2/functional-lecture02-deriv1.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,7 @@ $$ \frac{\frac{\begin{array}{ll}
\rightarrow
[? \alpha]} $$

$$ \text{we know that \text{{\texttt{1}}}} : \text{{\texttt{int}}}
$$
$$ \text{we know that \text{{\texttt{1}}}} : \text{{\texttt{int}}} $$

$$ \frac{\frac{\begin{array}{ll}
\frac{[?]}{\text{{\texttt{(+) x}}} :
Expand Down Expand Up @@ -86,8 +85,7 @@ $$ \frac{\frac{\begin{array}{ll}
\text{{\texttt{int}}}} & \frac{\,}{\text{{\texttt{1}}} :
\text{{\texttt{int}}}} \tiny{\text{(constant)}}
\end{array}}{\text{{\texttt{((+) x) 1}}} :
\text{{\texttt{int}}}}}{\text{\text{{\texttt{fun x -> ((+)
x)
\text{{\texttt{int}}}}}{\text{\text{{\texttt{fun x -> ((+) x)
1}}}} : \text{{\texttt{int}}} \rightarrow
\text{{\texttt{int}}}} $$

Expand Down
10 changes: 3 additions & 7 deletions chapter2/functional-lecture02.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,16 +15,12 @@ $$ \begin{matrix}
& \frac{[?]}{\text{{\texttt{fun x -> x}}} : [?]} & \text{use }
\rightarrow \text{ introduction:}\\\\\\
& \frac{\frac{\,}{\text{{\texttt{x}}} : a}
\tiny{x}}{\text{{\texttt{fun x -> x}}} : [?] \rightarrow
[?]}
& \frac{\,}{\text{{\texttt{x}}} : a} \tiny{x} \text{ matches
with }
\tiny{x}}{\text{{\texttt{fun x -> x}}} : [?] \rightarrow [?]}
& \frac{\,}{\text{{\texttt{x}}} : a} \tiny{x} \text{ matches with }
{{{\frac{\,}{x : a} \tiny{x}} \atop {\text{\textbar}}} \atop {e : b}}
\text{ since } e = \text{{\texttt{x}}}\\\\\\
& \frac{\frac{\,}{\text{{\texttt{x}}} : a}
\tiny{x}}{\text{{\texttt{fun x -> x}}} : a \rightarrow a}
&
\tiny{x}}{\text{{\texttt{fun x -> x}}} : a \rightarrow a} &
\text{since } b = a \text{ because } x : a \text{ matched with } e : b
\end{matrix} $$

Expand Down
24 changes: 8 additions & 16 deletions old_lectures_as_book.md
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,9 @@ $$ \frac{\frac{\begin{array}{ll}
\small{x}}{\text{go outdoor}}
\end{array}}{\text{nice view}}
\end{array}}{\text{happy}}}{\text{sunny} \rightarrow \text{happy}}
\small{\text{ using } x} $$Elimination rule for disjunction represents **reasoning by cases**.
\small{\text{ using } x} $$

Elimination rule for disjunction represents **reasoning by cases**.

How can we use the fact that it is sunny$\vee$cloudy (but not rainy)?

Expand All @@ -151,7 +153,6 @@ natural numbers:

$$ \frac{\begin{array}{rr}
p (0) &
{{{\frac{\,}{p(x)} \tiny{x}} \atop {\text{\textbar}}} \atop {p(x+1)}}
\end{array}}{p (n)} \text{ by induction, using } x $$

Expand Down Expand Up @@ -241,7 +242,6 @@ than these:

$$ \frac{\begin{array}{ll}
e_{1} : a &
{{{\frac{\,}{x : a} \tiny{x}} \atop {\text{\textbar}}} \atop {e_2 : b}}
\end{array}}{\text{{\texttt{let}} } x \text{{\texttt{=}}}
e_{1} \text{ \text{{\texttt{in}}} } e_{2} : b} $$
Expand All @@ -250,9 +250,7 @@ $$ \frac{\begin{array}{ll}
$\rightarrow$), and:

$$ \frac{\begin{array}{ll}
{{{\frac{\,}{x : a} \tiny{x}} \atop {\text{\textbar}}} \atop {e_1 : a}} &
{{{\frac{\,}{x : a} \tiny{x}} \atop {\text{\textbar}}} \atop {e_2 : b}}
\end{array}}{\text{{\texttt{let rec}} } x
\text{{\texttt{=}}} e_{1} \text{ \text{{\texttt{in}}} } e_{2}
Expand Down Expand Up @@ -361,16 +359,12 @@ $$ \begin{matrix}
& \frac{[?]}{\text{{\texttt{fun x -> x}}} : [?]} & \text{use }
\rightarrow \text{ introduction:}\\\\\\
& \frac{\frac{\,}{\text{{\texttt{x}}} : a}
\tiny{x}}{\text{{\texttt{fun x -> x}}} : [?] \rightarrow
[?]}
& \frac{\,}{\text{{\texttt{x}}} : a} \tiny{x} \text{ matches
with }
\tiny{x}}{\text{{\texttt{fun x -> x}}} : [?] \rightarrow [?]}
& \frac{\,}{\text{{\texttt{x}}} : a} \tiny{x} \text{ matches with }
{{{\frac{\,}{x : a} \tiny{x}} \atop {\text{\textbar}}} \atop {e : b}}
\text{ since } e = \text{{\texttt{x}}}\\\\\\
& \frac{\frac{\,}{\text{{\texttt{x}}} : a}
\tiny{x}}{\text{{\texttt{fun x -> x}}} : a \rightarrow a}
&
\tiny{x}}{\text{{\texttt{fun x -> x}}} : a \rightarrow a} &
\text{since } b = a \text{ because } x : a \text{ matched with } e : b
\end{matrix} $$

Expand Down Expand Up @@ -888,8 +882,7 @@ $$ \frac{\frac{\begin{array}{ll}
\rightarrow
[? \alpha]} $$

$$ \text{we know that \text{{\texttt{1}}}} : \text{{\texttt{int}}}
$$
$$ \text{we know that \text{{\texttt{1}}}} : \text{{\texttt{int}}} $$

$$ \frac{\frac{\begin{array}{ll}
\frac{[?]}{\text{{\texttt{(+) x}}} :
Expand Down Expand Up @@ -949,8 +942,7 @@ $$ \frac{\frac{\begin{array}{ll}
\text{{\texttt{int}}}} & \frac{\,}{\text{{\texttt{1}}} :
\text{{\texttt{int}}}} \tiny{\text{(constant)}}
\end{array}}{\text{{\texttt{((+) x) 1}}} :
\text{{\texttt{int}}}}}{\text{\text{{\texttt{fun x -> ((+)
x)
\text{{\texttt{int}}}}}{\text{\text{{\texttt{fun x -> ((+) x)
1}}}} : \text{{\texttt{int}}} \rightarrow
\text{{\texttt{int}}}} $$

Expand Down
9 changes: 9 additions & 0 deletions site/dune
Original file line number Diff line number Diff line change
Expand Up @@ -41,3 +41,12 @@
(action
(system
"pandoc -s --katex %{deps} -o %{target}")))

; (rule
; (alias old_lectures_as_book)
; (mode promote)
; (target old_lectures_as_book.hs)
; (deps old_lectures_as_book.md)
; (action
; (system
; "pandoc -s --katex --to native %{deps} -o %{target}")))
47 changes: 27 additions & 20 deletions site/old_lectures_as_book.html
Original file line number Diff line number Diff line change
Expand Up @@ -435,8 +435,9 @@ <h1 id="in-the-beginning-there-was-logos">1 In the Beginning there was
\small{x}}{\text{go outdoor}}
\end{array}}{\text{nice view}}
\end{array}}{\text{happy}}}{\text{sunny} \rightarrow \text{happy}}
\small{\text{ using } x} </span>Elimination rule for disjunction
represents <strong>reasoning by cases</strong>.</p>
\small{\text{ using } x} </span></p>
<p>Elimination rule for disjunction represents <strong>reasoning by
cases</strong>.</p>
<p>How can we use the fact that it is sunny<span
class="math inline">\vee</span>cloudy (but not rainy)?</p>
<p><span class="math display"> \frac{\begin{array}{rrl}
Expand All @@ -452,7 +453,10 @@ <h1 id="in-the-beginning-there-was-logos">1 In the Beginning there was
need one more kind of rules to do serious math: <strong>reasoning by
induction</strong> (it is somewhat similar to reasoning by cases).
Example rule for induction on natural numbers:</p>
<p>$$ x $$</p>
<p><span class="math display"> \frac{\begin{array}{rr}
p (0) &amp;
{{{\frac{\,}{p(x)} \tiny{x}} \atop {\text{\textbar}}} \atop {p(x+1)}}
\end{array}}{p (n)} \text{ by induction, using } x </span></p>
<p>So we get any <span class="math inline">p</span> for any natural
number <span class="math inline">n</span>, provided we can get it for
<span class="math inline">0</span>, and using it for <span
Expand Down Expand Up @@ -605,10 +609,20 @@ <h2 id="definitions">3.1 Definitions</h2>
definition.</p>
<p><strong>Definitions for expressions</strong> are introduced by rules
a bit more complex than these:</p>
<p>$$ $$</p>
<p><span class="math display"> \frac{\begin{array}{ll}
e_{1} : a &amp;
{{{\frac{\,}{x : a} \tiny{x}} \atop {\text{\textbar}}} \atop {e_2 : b}}
\end{array}}{\text{{\texttt{let}} } x \text{{\texttt{=}}}
e_{1} \text{ \text{{\texttt{in}}} } e_{2} : b} </span></p>
<p>(note that this rule is the same as introducing and eliminating <span
class="math inline">\rightarrow</span>), and:</p>
<p>$$ $$</p>
<p><span class="math display"> \frac{\begin{array}{ll}
{{{\frac{\,}{x : a} \tiny{x}} \atop {\text{\textbar}}} \atop {e_1 : a}}
&amp;
{{{\frac{\,}{x : a} \tiny{x}} \atop {\text{\textbar}}} \atop {e_2 : b}}
\end{array}}{\text{{\texttt{let rec}} } x
\text{{\texttt{=}}} e_{1} \text{ \text{{\texttt{in}}} } e_{2}
\: b} </span></p>
<p>We will cover what is missing in above rules when we will talk about
<strong>polymorphism.</strong>* Type definitions we have seen above are
<em>global</em>: they need to be at the top-level, not nested in
Expand Down Expand Up @@ -710,25 +724,20 @@ <h1 id="a-glimpse-at-type-inference">1 A Glimpse at Type Inference</h1>
<p>For a refresher, let’s try to use the rules we introduced last time
on some simple examples. Starting with <code>fun x -&gt; x</code>. <span
class="math inline">[?]</span> will mean “dunno yet”.</p>
$$
<span class="math display">\begin{matrix}
<p><span class="math display"> \begin{matrix}
&amp; \frac{[?]}{\text{{\texttt{fun x -&gt; x}}} : [?]} &amp;
\text{use }
\rightarrow \text{ introduction:}\\\\\\
&amp; \frac{\frac{\,}{\text{{\texttt{x}}} : a}
\tiny{x}}{\text{{\texttt{fun x -&gt; x}}} : [?] \rightarrow
[?]}
&amp; \frac{\,}{\text{{\texttt{x}}} : a} \tiny{x} \text{ matches
with }

\tiny{x}}{\text{{\texttt{fun x -&gt; x}}} : [?] \rightarrow [?]}
&amp; \frac{\,}{\text{{\texttt{x}}} : a} \tiny{x} \text{ matches with
}
{{{\frac{\,}{x : a} \tiny{x}} \atop {\text{\textbar}}} \atop {e : b}}
\text{ since } e = \text{{\texttt{x}}}\\\\\\
&amp; \frac{\frac{\,}{\text{{\texttt{x}}} : a}
\tiny{x}}{\text{{\texttt{fun x -&gt; x}}} : a \rightarrow a}
&amp;
\tiny{x}}{\text{{\texttt{fun x -&gt; x}}} : a \rightarrow a} &amp;
\text{since } b = a \text{ because } x : a \text{ matched with } e : b
\end{matrix}</span>
<p>$$</p>
\end{matrix} </span></p>
<p>Because <span class="math inline">a</span> is arbitrary, OCaml puts a
<em>type variable</em> <code>'a</code> for it:</p>
<div class="sourceCode" id="cb3"><pre
Expand Down Expand Up @@ -1186,8 +1195,7 @@ <h1 id="homework">6 Homework</h1>
\rightarrow
[? \alpha]} </span></p>
<p><span class="math display"> \text{we know that \text{{\texttt{1}}}} :
\text{{\texttt{int}}}
</span></p>
\text{{\texttt{int}}} </span></p>
<p><span class="math display"> \frac{\frac{\begin{array}{ll}
\frac{[?]}{\text{{\texttt{(+) x}}} :
\text{{\texttt{int}}} \rightarrow [? \alpha]} &amp;
Expand Down Expand Up @@ -1242,8 +1250,7 @@ <h1 id="homework">6 Homework</h1>
\text{{\texttt{int}}}} &amp; \frac{\,}{\text{{\texttt{1}}} :
\text{{\texttt{int}}}} \tiny{\text{(constant)}}
\end{array}}{\text{{\texttt{((+) x) 1}}} :
\text{{\texttt{int}}}}}{\text{\text{{\texttt{fun x -&gt; ((+)
x)
\text{{\texttt{int}}}}}{\text{\text{{\texttt{fun x -&gt; ((+) x)
1}}}} : \text{{\texttt{int}}} \rightarrow
\text{{\texttt{int}}}} </span></p>
<h1 id="chapter-3">Chapter 3</h1>
Expand Down

0 comments on commit 62dfb7d

Please sign in to comment.