Reed Mullanix
Reed Mullanix
Here's a more minimal repo: ``` def test : (x : type) × x := hcom {(x : type) × x} 0 1 ⊥ {j _ => [ j=0 =>...
After a bit of poking around, it seems that the crash happens when we try to evaluate the cap of the `Box` by `test`...
Oh that could totally be it!
The plan is to go back through once the rest of the work is done and actually implement those, so FIXME makes for an easy grep.
So bundling up all of the individual motives is proving tricky! My initial plan was to use the classic ```agda infixl 2 _▶_ data Con : Set where ∙ :...
Consider ``` def example : type := sig (p : 𝕀 → ℕ) ``` This will elaborate to a code, which will then require all of the fields of the...
Sorry, misunderstood your request! With `deftype`, we'd elaborate this as a `Signature`, which should allow us to elaborate the fields as types, which solves the problem.
I have some code in `lsp-mode` for auto-updating if you want to use that as a base. It should be available here: https://github.com/emacs-lsp/lsp-mode/blob/85682e663fe4307f890a65ef207fbe03eb506724/lsp-fsharp.el#L191
I can reproduce this with `cabal build`, however, `stack build` seems to work. Note that this is on OSX, so it doesn't appear to be limited to `nix`.
Perhaps a more generalized version could be added, along with something like: ``` data Bound a = Inclusive a | Exclusive a ``` If this was added, I still think...