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

[fblanqui]

[NotBad4U]

Would it be possible to add more information about the assert command when it fails? For example:

assert ⊢ true : ℕ; // case 1
assert ⊢ 1 + 1 ≡ 1; // case 2

The only output we have when an assertion fails is the message Assertion failed. Would it be possible to output in case 1 the type inferred by Lambdapi, and in case 2, what are the left and right evaluation? It can be done by hand for now, but I believe that it should be the correct behavior of the assert command.

[fblanqui]

The assert's this issue is about are the OCaml assert's used to implement Lambdapi. For feature requests concerning the Lambdapi commands assert/assertnot, please open a distinct issue.

[ejgallego]

Flèche should help with this, due to the way we encapsulate exceptions.