Jacob Thomas Errington
Jacob Thomas Errington
The `--stop` option was added to Harpoon to assist in debugging command transcripts, to make Harpoon exit on the first command that produces an exception. The problem is that errors...
The current bash script for testing has been a problem almost every time we try to upgrade it, due to cross-platform compatibility issues. I believe that it should be replaced...
Bound mvars from PiBox types are too eagerly renamed. For example, consider the type `{S : |- step M M'} [ |- halts M' ] -> [|- halts M]` and...
We currently forbid IH appeals in `suffices by` because the interaction with the totality checker is not obvious. It's complicated enough to get termination checking to work in ordinary `by`,...
Presently there are the errors `TooManyMetaObj` and `MissingMetaObj` thrown in `elMetaSpine` in `reconstruct.ml` when there are, respectively, too many arguments and too few arguments supplied to a data constructor. The...
The pretty-printer currently calls normalization functions when it encounters clearly non-normal terms (e.g. closures). This makes debugging difficult because it means we can't call any pretty-printing functions from `whnf.ml` where...
## Background Consider the type `tau = [|- oft M A] -> [|- oft M A]`. It contains free metavariables `M` and `A`, which are automatically quantified by abstraction. The...
#182 outlines an implementation plan for a simple way to improve bound variable type inference in the single-element schema case. I have thought a bit about how to make such...
Consider the recursive call for type uniqueness, which looks like this in the t_lam case: ``` unique [g, b : block x : term, u : hastype _ _ |-...
Load this signature ``` LF a : type = ; schema ctx = a; LF nat : type = | zero : nat | succ : nat → nat ;...