Use markdown for exercises, since it works fine out of the box.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
2d640f2e6a
commit
a6f3bccf64
|
@ -178,5 +178,5 @@ TPlusI @ type(plus(?e_1, ?e_2), number) <-
|
||||||
{{< /bergamot_preset >}}
|
{{< /bergamot_preset >}}
|
||||||
|
|
||||||
{{< bergamot_exercise label="bergamot; sample exercise" preset="intro-preset" id="exercise-2" >}}
|
{{< bergamot_exercise label="bergamot; sample exercise" preset="intro-preset" id="exercise-2" >}}
|
||||||
Try typing <code>1+1</code> into the input field!
|
Try typing `1+1` into the input field!
|
||||||
{{< /bergamot_exercise >}}
|
{{< /bergamot_exercise >}}
|
||||||
|
|
|
@ -120,16 +120,16 @@ TNumber @ type(lit(?n), number) <- num(?n);
|
||||||
|
|
||||||
{{< bergamot_exercise label="bergamot; tweaking notation" preset="notation-preset" id="exercise-1" >}}
|
{{< bergamot_exercise label="bergamot; tweaking notation" preset="notation-preset" id="exercise-1" >}}
|
||||||
Bergamot, the interactive tool I've developed for doing exercises, supports
|
Bergamot, the interactive tool I've developed for doing exercises, supports
|
||||||
customizing the notation for rules. Try changing the \(:\) symbol to
|
customizing the notation for rules. Try changing the \\(:\\) symbol to
|
||||||
the \(\sim\) symbol (denoted in latex as <code>\sim</code>).<br>
|
the \\(\\sim\\) symbol (denoted in latex as `\sim`).
|
||||||
<br>
|
|
||||||
To change the way that rules are rendered, click the "Presentation Rules"
|
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
|
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.
|
pretty-printing a fair amount of the standard programming languages notation.
|
||||||
Scroll down to <code>LatexTypeBin</code>, and change <code>:</code> to
|
Scroll down to `LatexTypeBin`, and change `:` to
|
||||||
<code>\\sim</code> on that line (the extra backslash is to handle string
|
`\\sim` on that line (the extra backslash is to handle string
|
||||||
escaping). Now try typing numbers into the input box; you should see
|
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 >}}
|
{{< /bergamot_exercise >}}
|
||||||
|
|
||||||
One more thing. So far, we've only written down one claim: the value 1 is a number.
|
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" >}}
|
{{< 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
|
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
|
above. I've provided the rules for numbers; the rules for strings should be quite
|
||||||
similar.<br>
|
similar.
|
||||||
<br>
|
|
||||||
In Bergamot, the claim that an expression <code>e</code> has type <code>t</code>
|
In Bergamot, the claim that an expression `e` has type `t`
|
||||||
is written as <code>type(e, t)</code>. A rule looks like <code>RuleName @ conclusion <- premise1, premise2;</code>.
|
is written as `type(e, t)`. A rule looks like `RuleName @ conclusion <- premise1, premise2;`.
|
||||||
Thus, the rule <pre><code>TNumber @ type(lit(?n), number) <- num(?n);
|
Thus, the rule
|
||||||
</code></pre>
|
|
||||||
Has one premise, that the term \(n\) is a number, and the conclusion is that
|
```
|
||||||
a number literal has type \(\text{number}\). The <code>num</code> condition
|
TNumber @ type(lit(?n), number) <- num(?n);
|
||||||
is a Bergamot builtin, corresponding to our earlier notation of \(n \in \texttt{Num}\).
|
```
|
||||||
It holds for all numbers: it's always true that <code>num(1)</code>, <code>num(2)</code>,
|
|
||||||
etc. The equivalent builtin for something being a string is <code>str</code>.<br>
|
Has one premise, that the term \\(n\\) is a number, and the conclusion is that
|
||||||
<br>
|
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`.
|
||||||
|
|
||||||
To edit the rules in Bergamot, click the "Editor" button in the "Rules"
|
To edit the rules in Bergamot, click the "Editor" button in the "Rules"
|
||||||
section. You will need to add two rules, just like we did for numbers:
|
section. You will need to add two rules, just like we did for numbers:
|
||||||
a rule for string literals (something like \(\texttt{"Hello"} : \text{string}\),
|
a rule for string literals (something like \\(\\texttt{\"Hello\"} : \\text{string}\\),
|
||||||
but more general) and for adding two strings together. I suggest naming
|
but more general) and for adding two strings together. I suggest naming
|
||||||
these two rules <code>TString</code> and <code>TPlusS</code> respectively.<br>
|
these two rules `TString` and `TPlusS` respectively.
|
||||||
<br>
|
|
||||||
When you're done, you should be able to properly determine the types of
|
When you're done, you should be able to properly determine the types of
|
||||||
expressions such as <code>"Hello"</code> and <code>"Hello" + "World"</code>.
|
expressions such as `"Hello"` and `"Hello" + "World"`.
|
||||||
{{< /bergamot_exercise >}}
|
{{< /bergamot_exercise >}}
|
||||||
|
|
||||||
These rules generally work in other languages. Things get more complicated in languages like Java and Rust,
|
These rules generally work in other languages. Things get more complicated in languages like Java and Rust,
|
||||||
|
|
|
@ -6,7 +6,7 @@
|
||||||
{{ if or (eq (.Get "label") "") (eq (.Get "label") nil) }}{{ else }}({{ .Get "label" }}){{ end }}:
|
{{ if or (eq (.Get "label") "") (eq (.Get "label") nil) }}{{ else }}({{ .Get "label" }}){{ end }}:
|
||||||
</span>
|
</span>
|
||||||
</summary>
|
</summary>
|
||||||
{{ .Inner }}
|
{{ transform.Markdownify .Inner }}
|
||||||
|
|
||||||
<div class="bergamot-button-group">
|
<div class="bergamot-button-group">
|
||||||
{{ if or (eq (.Get "preset") "") (eq (.Get "preset") nil) }}
|
{{ if or (eq (.Get "preset") "") (eq (.Get "preset") nil) }}
|
||||||
|
|
Loading…
Reference in New Issue
Block a user