diff --git a/content/blog/00_types_intro.md b/content/blog/00_types_intro.md
index db1fa57..751e748 100644
--- a/content/blog/00_types_intro.md
+++ b/content/blog/00_types_intro.md
@@ -178,5 +178,5 @@ TPlusI @ type(plus(?e_1, ?e_2), number) <-
{{< /bergamot_preset >}}
{{< bergamot_exercise label="bergamot; sample exercise" preset="intro-preset" id="exercise-2" >}}
-Try typing 1+1
into the input field!
+Try typing `1+1` into the input field!
{{< /bergamot_exercise >}}
diff --git a/content/blog/01_types_basics.md b/content/blog/01_types_basics.md
index 59e11bc..e319558 100644
--- a/content/blog/01_types_basics.md
+++ b/content/blog/01_types_basics.md
@@ -120,16 +120,16 @@ TNumber @ type(lit(?n), number) <- num(?n);
{{< bergamot_exercise label="bergamot; tweaking notation" preset="notation-preset" id="exercise-1" >}}
Bergamot, the interactive tool I've developed for doing exercises, supports
-customizing the notation for rules. Try changing the \(:\) symbol to
-the \(\sim\) symbol (denoted in latex as \sim
).
-
+customizing the notation for rules. Try changing the \\(:\\) symbol to
+the \\(\\sim\\) symbol (denoted in latex as `\sim`).
+
To change the way that rules are rendered, click the "Presentation Rules"
tab in the "Rules" section. There will be a lot there: I've added rules for
pretty-printing a fair amount of the standard programming languages notation.
-Scroll down to LatexTypeBin
, and change :
to
-\\sim
on that line (the extra backslash is to handle string
+Scroll down to `LatexTypeBin`, and change `:` to
+`\\sim` on that line (the extra backslash is to handle string
escaping). Now try typing numbers into the input box; you should see
-something like \(1 \sim \text{number} \)
+something like \\(1 \\sim \text{number} \\)
{{< /bergamot_exercise >}}
One more thing. So far, we've only written down one claim: the value 1 is a number.
@@ -326,26 +326,30 @@ TPlusI @ type(plus(?e_1, ?e_2), number) <-
{{< bergamot_exercise label="bergamot; adding rules for strings" preset="string-preset" id="exercise-2" >}}
Try writing the Bergamot rules that correspond to the inference rule for strings
above. I've provided the rules for numbers; the rules for strings should be quite
-similar.
-
-In Bergamot, the claim that an expression e
has type t
-is written as type(e, t)
. A rule looks like RuleName @ conclusion <- premise1, premise2;
.
-Thus, the rule
TNumber @ type(lit(?n), number) <- num(?n);
-
-Has one premise, that the term \(n\) is a number, and the conclusion is that
-a number literal has type \(\text{number}\). The num
condition
-is a Bergamot builtin, corresponding to our earlier notation of \(n \in \texttt{Num}\).
-It holds for all numbers: it's always true that num(1)
, num(2)
,
-etc. The equivalent builtin for something being a string is str
.TString
and TPlusS
respectively."Hello"
and "Hello" + "World"
.
+expressions such as `"Hello"` and `"Hello" + "World"`.
{{< /bergamot_exercise >}}
These rules generally work in other languages. Things get more complicated in languages like Java and Rust,
diff --git a/layouts/shortcodes/bergamot_exercise.html b/layouts/shortcodes/bergamot_exercise.html
index 817c3ba..444406d 100644
--- a/layouts/shortcodes/bergamot_exercise.html
+++ b/layouts/shortcodes/bergamot_exercise.html
@@ -6,7 +6,7 @@
{{ if or (eq (.Get "label") "") (eq (.Get "label") nil) }}{{ else }}({{ .Get "label" }}){{ end }}:
- {{ .Inner }}
+ {{ transform.Markdownify .Inner }}