From 62dfb7d3612ced8e3d3e1cc12c9e4bc4ffa02d31 Mon Sep 17 00:00:00 2001 From: Lukasz Stafiniak Date: Thu, 26 Oct 2023 13:08:56 +0200 Subject: [PATCH] Remove empty lines from inside equation blocks Works in VS Code markdown preview, but breaks pandoc conversion. --- chapter1/functional-lecture01.md | 8 ++--- chapter2/functional-lecture02-deriv1.md | 6 ++-- chapter2/functional-lecture02.md | 10 ++---- old_lectures_as_book.md | 24 +++++-------- site/dune | 9 +++++ site/old_lectures_as_book.html | 47 ++++++++++++++----------- 6 files changed, 52 insertions(+), 52 deletions(-) diff --git a/chapter1/functional-lecture01.md b/chapter1/functional-lecture01.md index c9eecf2..1468205 100644 --- a/chapter1/functional-lecture01.md +++ b/chapter1/functional-lecture01.md @@ -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)? @@ -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 $$ @@ -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} $$ @@ -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} diff --git a/chapter2/functional-lecture02-deriv1.md b/chapter2/functional-lecture02-deriv1.md index 6c7613b..fb2ba3f 100644 --- a/chapter2/functional-lecture02-deriv1.md +++ b/chapter2/functional-lecture02-deriv1.md @@ -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}}} : @@ -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}}}} $$ diff --git a/chapter2/functional-lecture02.md b/chapter2/functional-lecture02.md index 539ee31..ba51f84 100644 --- a/chapter2/functional-lecture02.md +++ b/chapter2/functional-lecture02.md @@ -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} $$ diff --git a/old_lectures_as_book.md b/old_lectures_as_book.md index cf748c5..bee13ff 100644 --- a/old_lectures_as_book.md +++ b/old_lectures_as_book.md @@ -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)? @@ -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 $$ @@ -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} $$ @@ -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} @@ -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} $$ @@ -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}}} : @@ -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}}}} $$ diff --git a/site/dune b/site/dune index 205622a..db1800a 100644 --- a/site/dune +++ b/site/dune @@ -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}"))) diff --git a/site/old_lectures_as_book.html b/site/old_lectures_as_book.html index 574ac53..10aaa1c 100644 --- a/site/old_lectures_as_book.html +++ b/site/old_lectures_as_book.html @@ -435,8 +435,9 @@

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} 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\veecloudy (but not rainy)?

\frac{\begin{array}{rrl} @@ -452,7 +453,10 @@

1 In the Beginning there was need one more kind of rules to do serious math: reasoning by induction (it is somewhat similar to reasoning by cases). Example rule for induction on natural numbers:

-

$$ x $$

+

\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

So we get any p for any natural number n, provided we can get it for 0, and using it for 3.1 Definitions

definition.

Definitions for expressions are introduced by rules a bit more complex 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}

(note that this rule is the same as introducing and eliminating \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} + \: b}

We will cover what is missing in above rules when we will talk about polymorphism.* Type definitions we have seen above are global: they need to be at the top-level, not nested in @@ -710,25 +724,20 @@

1 A Glimpse at Type Inference

For a refresher, let’s try to use the rules we introduced last time on some simple examples. Starting with fun x -> x. [?] will mean “dunno yet”.

-$$ -\begin{matrix} +

\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} -

$$

+\end{matrix}

Because a is arbitrary, OCaml puts a type variable 'a for it:

6 Homework
 \rightarrow
    [? \alpha]} 

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

+\text{{\texttt{int}}} 

 
 \frac{\frac{\begin{array}{ll}
      \frac{[?]}{\text{{\texttt{(+) x}}} :
      \text{{\texttt{int}}} \rightarrow [? \alpha]} &
@@ -1242,8 +1250,7 @@ 
6 Homework

      \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}}}} 

 
Chapter 3