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
[Γ, 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:
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:
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 recs! which is because you can mix
rec/proof, or
inductive/coinductive/stratified,
within a block.