a few undocumented beluga features

tuesday 12 july 2022

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


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.