Beluga
Beluga copied to clipboard
Beluga-lang
Contextual types meet mechanized metatheory!
``` LF t : type = | c : ({x : _} t) -> t ; ``` ``` Uncaught exception. Please report this as a bug. File "src/core/index.ml", line 357,...
I'm trying to go through the NbE example, and got an internal error. I've simplified it to this: ``` $ cat bug.bel LF tm : type = | abs :...
The following dune environment variables are set in the `core`, `harpoon` and `optparser` packages. These globally disable compilation warnings such as unused variables. However, what I find alarming is that...
Consider the following Twelf excerpt from the mechanization of Standard ML. Here, `unmap-tequiv` is proved in a world that includes `unmap-bind`: ``` %block unmap-bind : some {K:kind} {B:etp} {Dmap:tunmap B...
Context variable checking against context schemas should support schema subsumption. Let `schema G1 = some [...S1] block (...B1)` and `schema G2 = some [...S2] block (...B2)` be context schemas, with...
Load the following signature: ``` LF kind : type = | sigma : kind -> (con -> kind) -> kind and con : type = ; --name kind K. --name...
In `Weak_Normalization.bel`, the main proof makes the term `M` decrease, but I can incorrectly claim that it is the context `g` that's decreasing. https://github.com/Beluga-lang/Beluga/blob/1d39095c99dc255d972a339d447dc04286d8c13f/examples/literate_beluga/2Advanced/Weak_Normalization.bel#L157 i.e., Beluga accepts the `/ total...
`beluga-mode`'s holes feature does not work after the first load as of https://github.com/Beluga-lang/Beluga/commit/1d39095c99dc255d972a339d447dc04286d8c13f because the elisp assumes that holes are numbered starting from 0 but the ocaml uses a single...
 For people who want an editor from later than last century. I've created the extension package (.vsix) file and I can give you guys the source code/package if anyone...
Hello, I'm having trouble building Beluga on WSL2, Ubuntu. I'm sure I'm just doing something wrong with opam - I've never used it before. Rather than try to troubleshoot, would...
