Alessio Coltellacci

icon indicating a website link https://notbad4u.github.io/my-resume/

icon company Inria icon location Nancy icon location I'm waiting for Godot. PhD student

Results 54 comments of Alessio Coltellacci

inconsistent lsp diagnostic locations

It is a known issue, and it also affects VSCode, but in a less critical way than Emacs or Zed. If you look at your second screenshot, you can notice...

improve applicability of the apply tactic

Could you describe what this PR will change on the `apply` tactic?

evaluation of lambda body

Hi, for me, it has the correct behavior because you use an unnamed pattern variable `test _`, so it will unify with any term and use the modifier `sequential`.

the LSP server returns no feedback in case of "assert false"

Would it be possible to add more information about the `assert` command when it fails? For example: ``` assert ⊢ true : ℕ; // case 1 assert ⊢ 1 +...