Jacob Thomas Errington

The type error is a mismatch between `term-eq ?E ?E` and `term-eq M[N'] M[N']` so Beluga hasn't even unified the arguments because there is a head mismatch. It really seems...

Given that the old-style Emacs interactive mode has been largely replaced by Harpoon, this is a low-priority issue.

Given that `--stop` is largely a debugging tool, I've made this issue low-priority for now.

That's exactly my concern with using Python. I believe macOS still ships Python 2, so we still have the same portability issue with supporting macOS. I think that writing the...

Throughout the development of Harpoon, we have realized that holes in synthesizable positions is a bad idea, broadly speaking, because of uninstantiated unification variables. Instead, this issue should be about...

The way Beluga deals with with out-of-scope metavariables is kind of weird. It doesn't immediately produce an error, because there's one situation where free metavariables are actually important, and that's...

@marcelgoh Yep. Using `DynArray.insert s.remaining_subgoals 0 g` should do the trick.

This issue is less serious than I first thought. Binding `a` in the right place gives ``` kind : type. con : type. lam : kind -> (con -> con)...

That definitely seems wrong, and it's probably related. My guess is that coverage checking for substitution variables is plain broken at the moment.

@durka and I thought about this somewhat when we discovered that the edit system currently in JVS is totally unsafe: anyone can edit anything and no record of the edits...