several of these are in the examples, just not in the documentation. but some of them i did find while looking through the parser.

## 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:

```
let [Γ, b : block (x : term, t : oft x A[..]) ⊢ X] = blah in
: term, t : oft x A[..] ⊢ X[.., <x; t>]]
[Γ, x
% but equivalent to this, but clearer (imo)
let [Γ, block (x : term, t : oft x A[..]) ⊢ X[.., b.x, b.t]] = blah in
: term, t : oft x A[..] ⊢ X] [Γ, 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:

```
case [Γ ⊢ #p] of
#p : [Γ ⊢ term]}
| {: term ⊢ #p[..]] ⇒ ?body [Γ, y
```

## mutual recursion

of course this exists. but it’s not mentioned anywhere in the documentation for some reason. the syntax is this:

```
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.