diff --git a/assets/scss/bergamot.scss b/assets/scss/bergamot.scss index acb740a..9914bc4 100644 --- a/assets/scss/bergamot.scss +++ b/assets/scss/bergamot.scss @@ -7,8 +7,10 @@ .bergamot-section-heading { margin-bottom: 0.5em; - font-family: sans-serif; - font-weight: normal; + font-family: $font-body; + font-style: normal; + font-weight: bold; + font-size: 1.25em; } .bergamot-section { @@ -41,6 +43,14 @@ flex-basis: 0; } + .bergamot-rule-section { + .bergamot-rule-section-name { + text-align: center; + margin: 0.25em; + font-weight: bold; + } + } + .bergamot-selector { button { @include var(background-color, background-color); diff --git a/content/blog/01_types_basics.md b/content/blog/01_types_basics.md index 0c3f638..bf42207 100644 --- a/content/blog/01_types_basics.md +++ b/content/blog/01_types_basics.md @@ -442,9 +442,33 @@ and already be up-to-speed on a big chunk of the content. #### Playground {{< bergamot_widget id="widget-one" query="" >}} -TInt @ type(intlit(?n), tint) <-; -TString @ type(strlit(?s), tstr) <-; -TPlusI @ type(plus(?e_1, ?e_2), tint) <- type(?e_1, tint), type(?e_2, tint); -TPlusS @ type(plus(?e_1, ?e_2), tstr) <- type(?e_1, tstr), type(?e_2, tstr); +section "" { + TNumber @ type(?Gamma, intlit(?n), number) <-; + TString @ type(?Gamma, strlit(?s), string) <-; + TVar @ type(?Gamma, var(?x), ?tau) <- inenv(?x, ?tau, ?Gamma); + TPlusI @ type(?Gamma, plus(?e_1, ?e_2), number) <- + type(?Gamma, ?e_1, number), type(?Gamma, ?e_2, number); + TPlusS @ type(?Gamma, plus(?e_1, ?e_2), string) <- + type(?Gamma, ?e_1, string), type(?Gamma, ?e_2, string); +} +section "" { + TPair @ type(?Gamma, pair(?e_1, ?e_2), tpair(?tau_1, ?tau_2)) <- + type(?Gamma, ?e_1, ?tau_1), type(?Gamma, ?e_2, ?tau_2); + TFst @ type(?Gamma, fst(?e), ?tau_1) <- + type(?Gamma, ?e, tpair(?tau_1, ?tau_2)); + TSnd @ type(?Gamma, snd(?e), ?tau_2) <- + type(?Gamma, ?e, tpair(?tau_1, ?tau_2)); +} +section "" { + TAbs @ type(?Gamma, abs(?x, ?tau_1, ?e), tarr(?tau_1, ?tau_2)) <- + type(extend(?Gamma, ?x, ?tau_1), ?e, ?tau_2); + TApp @ type(?Gamma, app(?e_1, ?e_2), ?tau_2) <- + type(?Gamma, ?e_1, tarr(?tau_1, ?tau_2)), type(?Gamma, ?e_2, ?tau_1); +} + +section "" { + GammaTake @ inenv(?x, ?tau_1, extend(?Gamma, ?x, ?tau_1)) <-; + GammaSkip @ inenv(?x, ?tau_1, extend(?Gamma, ?y, ?tau_2)) <- inenv(?x, ?tau_1, ?Gamma); +} {{< /bergamot_widget >}} diff --git a/layouts/shortcodes/bergamot_widget.html b/layouts/shortcodes/bergamot_widget.html index 1aff8e6..eb130e5 100644 --- a/layouts/shortcodes/bergamot_widget.html +++ b/layouts/shortcodes/bergamot_widget.html @@ -13,8 +13,6 @@ LatexInt @ latex(?i, ?l) <- int(?i), tostring(?i, ?l); LatexStr @ latex(?s, ?l) <- str(?s), escapestring(?s, ?l_1), latexifystring(?s, ?l_2), join(["\\\\texttt{\\"", ?l_2, "\\"}"], ?l); LatexMeta @ latex(metavariable(?l), ?l) <-; - LatexSym @ latex(?s, ?l) <- sym(?s), tostring(?s, ?l_1), join(["\\\\text{", ?l_1,"}"], ?l); - LatexCall @ latex(?c, ?l) <- call(?c, ?n, ?ts), nonempty(?ts), latexlist(?ts, ?lts_1), intercalate(", ", ?lts_1, ?lts_2), join(?lts_2, ?lts_3), join(["\\\\text{", ?n, "}", "(", ?lts_3, ")"], ?l); LatexIntLit @ latex(intlit(?i), ?l) <- latex(?i, ?l); LatexStrLit @ latex(strlit(?s), ?l) <- latex(?s, ?l); LatexPlus @ latex(plus(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join([?l_1, " + ", ?l_2], ?l); @@ -32,7 +30,11 @@ LatexTypeInenv @ latex(inenv(?x, ?t, ?G), ?l) <-latex(?x, ?l_x), latex(?t, ?l_t), latex(?G, ?l_G), join([?l_x, " : ", ?l_t, " \\\\in ", ?l_G], ?l); LatexTypeBin @ latex(type(?e, ?t), ?l) <- latex(?e, ?l_e), latex(?t, ?l_t), join([?l_e, " : ", ?l_t], ?l); - LatexTypeTer @ latex(type(?G, ?e, ?t), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?t, ?l_t), join([?l_G, " \\\\vdash ", ?l_e, " : ", ?l_t], ?l);`; + LatexTypeTer @ latex(type(?G, ?e, ?t), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?t, ?l_t), join([?l_G, " \\\\vdash ", ?l_e, " : ", ?l_t], ?l); + + LatexSym @ latex(?s, ?l) <- sym(?s), tostring(?s, ?l_1), join(["\\\\text{", ?l_1,"}"], ?l); + LatexCall @ latex(?c, ?l) <- call(?c, ?n, ?ts), nonempty(?ts), latexlist(?ts, ?lts_1), intercalate(", ", ?lts_1, ?lts_2), join(?lts_2, ?lts_3), join(["\\\\text{", ?n, "}", "(", ?lts_3, ")"], ?l); + `; var app = Elm.Main.init({ node: document.getElementById('{{ .Get "id" }}'), flags: { renderRules, rules: '{{- strings.Trim .Inner " \\n" -}}', query: '{{ .Get "query" }}' }