Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Update use of the bergamot widget

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2023-12-21 17:26:19 -08:00
parent 5c83f234c6
commit a83268a6e3
3 changed files with 45 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files

32
content/blog/01_types_basics.md
View File

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