From 8d401ab404052bc6a9ba6b898452bff6d047ccd7 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 17 Sep 2022 20:56:50 +0200
Subject: [PATCH] """finish""" old beluga post

---
 posts/2022-03-14-digitle-in-maude.md |  2 +-
 posts/2022-07-12-beluga.md           | 76 ++++++++++++++++++++++++++++
 2 files changed, 77 insertions(+), 1 deletion(-)
 create mode 100644 posts/2022-07-12-beluga.md

diff --git a/posts/2022-03-14-digitle-in-maude.md b/posts/2022-03-14-digitle-in-maude.md
index c79ff0f..88351a4 100644
--- a/posts/2022-03-14-digitle-in-maude.md
+++ b/posts/2022-03-14-digitle-in-maude.md
@@ -1,7 +1,7 @@
 ---
 title: digitle in maude
 date: 2022-03-14
-tags: [maude, computer]
+tags: [maude, computer, cool languages]
 ...
 
 so you know [digitle] right. it's the countdown numbers round.
diff --git a/posts/2022-07-12-beluga.md b/posts/2022-07-12-beluga.md
new file mode 100644
index 0000000..9e44cc2
--- /dev/null
+++ b/posts/2022-07-12-beluga.md
@@ -0,0 +1,76 @@
+---
+date:  2022-07-12
+title: a few undocumented beluga features
+tags:  [computer, beluga, cool languages]
+toc: true
+...
+
+
+several of these are in the [examples], just not in the documentation. but some
+of them i did find while looking through the parser.
+
+[examples]: https://github.com/Beluga-lang/Beluga/tree/master/examples
+
+
+## unicode
+
+you can call your context variables `Γ` and it works just fine.
+you can also use `→` and `⇒` and `⊢` if they are legible in the font you're
+using.
+
+
+## block values in substitutions
+
+a lot of the time you have a variable typed like
+`\[Γ, b : block (x : term, t : oft x A[..]) ⊢ ty]`,
+but you actually need a
+`\[Γ, x : term, t : oft x A[..] ⊢ ty]`,
+with the block flattened out. or vice versa.
+or you want to substitute the block more conveniently.
+
+for this purpose, there is actually a block literal syntax `<a; b; c>` usable
+in substitutions:
+
+```beluga
+let [Γ, b : block (x : term, t : oft x A[..]) ⊢ X] = blah in
+[Γ, x : term, t : oft x A[..] ⊢ X[.., <x; t>]]
+
+% but equivalent to this, but clearer (imo)
+let [Γ, block (x : term, t : oft x A[..]) ⊢ X[.., b.x, b.t]] = blah in
+[Γ, x : term, t : oft x A[..] ⊢ X]
+```
+
+## explicit binders before patterns
+
+sometimes in a case expression, the type of the pattern variables is too hard
+for beluga to work out on its own. in this case you get an error message about
+a stuck unification problem.
+
+most of the time you can get out of this by writing the types of some variables
+explicitly. the syntax is like a forall-type:
+
+```beluga
+case [Γ ⊢ #p] of
+| {#p : [Γ ⊢ term]}
+  [Γ, y : term ⊢ #p[..]] ⇒ ?body
+```
+
+
+## mutual recursion
+
+of course this exists. but it's not mentioned anywhere in the documentation for
+some reason. the syntax is this:
+
+```beluga
+LF  term : type = …
+and elim : type = …;
+
+rec     eval-term : (Γ : ctx) [Γ ⊢ term] → [Γ ⊢ value] = …
+and rec eval-elim : (Γ : ctx) [Γ ⊢ elim] → [Γ ⊢ value] = …;
+
+inductive     ReduceTerm : (Γ : ctx) [Γ ⊢ term] → ctype = …
+and inductive ReduceElim : (Γ : ctx) [Γ ⊢ elim] → ctype = …;
+```
+
+two `rec`s! which is because you can mix `rec`/`proof`, or
+`inductive`/`coinductive`/`stratified`, within a block.