Resolve "Add `Eq` and definitional Proof-Irrelevance" ✨️

Closes #57, #63, and #20 🐔️👍️
Approved-by: v-lafeychine <vincent.lafeychine@proton.me>
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: loutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰



* chore: split example file contraposition.mdln meaningfuly and remove already-defined axioms

* Apply 9 suggestion(s) to 3 file(s)

* Apply 11 suggestion(s) to 4 file(s)

* chore(kernel): add documentation

* chore(kernel): Refactor axiom into own mod

* feat(examples): add more examples

* chore(kernel): Remove let chains in if, because of Deref-missing implementation

* Apply 1 suggestion(s) to 1 file(s)

* Apply 1 suggestion(s) to 1 file(s)

* fix(kernel): comment syntax

* fix(kernel): proof-irrelevance

* fix(kernel): slur in comment

* fix(kernel): fix comment

* chore(kernel): add tests

* fix(kernel): fix relevance for wildcard terms

* feat(kernel): add relevance tag to terms

* fix(examples): fix irrelevance example

* feat(example): add irrelevance example

* fix(kernel): avoid infinite looping

* fix(kernel): fix `is_prop_term`

* feat(kernel): add `is_prop_term` and `is_prop_type`

* feat(kernel): better recursor pattern recognition

* feat(examples): add example using `Eq`

* fix(kernel): whnf reduction on recursors

* fix(kernel): `Eq_rec` type

* feat(kernel): add reduction rule for `Eq_rec`

* fix(kernel): `Eq` type

* feat(kernel): add `Eq` type

* Resolve "LSP: Proof-of-concept" ✨️
Closes #20 🐔️👍️
Approved-by: aalbert <augustin.albert@bleu-azure.fr>
Approved-by: belazy <aarthuur01@gmail.com>
Approved-by: loutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰

* chore(tilleul): fix typos in documentation

* chore(tilleul): Add axioms

* chore(tilleul): Add global server tests on unexpected queries

* chore(tilleul): Add UTF-8 message test

* chore(tilleul): Add connection tests

* chore(tilleul): Add message write/read test

* chore(tilleul): Add dispatcher tests

* fix(tilleul): Documentation

* feat(editors): Add emacs integration

* feat(tilleul): Add server mock

* chore(coverage): Ignore log functions

* feat(tilleul): Transform Connection into a trait

* feat(tilleul): Add complete LSP lifecycle

* chore(tilleul): Rename backend crate to lsp and payload crate to message, madedocumentation and fix clippy issues

* chore(tilleul): Rename server crate in backend, made a directory for tilleul

* feat(tilleul): Add WaitingForInitialisation + Initialised states

* chore(tilleul): Fix moved dependencies

* feat(lsp): Add early parsing from tilleul

* feat(lsp): Add notification dispatcher + Improve request dispatcher

* refactor(lsp): Add LanguageServerBackend

* chore(lsp): Remove LSP states

* chore(lsp): Improve request handling

* feat(lsp): Early request dispatcher

* feat(lsp): Add early message handling + Rename message into payload

* fix(cargo): Use workspace for tilleul

* fix(cargo): Use workspace for tilleul

* feat(lsp): Add early LSP stages

* feat(lsp): Add exit notification

* feat(lsp): Threads + Early IO server

* feat(lsp): Initial commit