Reformulate borrowing using the T-necessity modality

[vekatze]

This PR reformulates the let-on stuff (or "borrowing") via the Curry-Howard correspondence of the T-necessity modality.

Docs

Here

Summary

• The T-necessity modality in Neut is written as meta {..}
• Terms of type meta {..} are introduced using box and eliminated using letbox / letbox-T
  • The axiom K can be proved via box and letbox
  • The axiom T can be proved via letbox-T
• Terms of type meta A can also be introduced using quote {..} when the type A is "simple"
  • e.g. quote {True}: meta bool
  • quote is technically unnecessary (just a shorthand)
• Introduction/Elimination of the modality is subject to certain conditions around layers.
• &a in Neut is now understood as a "structual necessity"
  • (A necessity that can only be used structurally)
• let-on is now decomposed into quote and letbox-T

Inference Rules

meta

Γ1; ...; Γn ⊢ t: type
-------------------------- (□-form)
Γ1; ...; Γn ⊢ meta t: type

box

Γ1; ...; Γn; Δ ⊢ e1: a
------------------------------------- (□-intro)
Γ1; ...; Γn, &Δ ⊢ box Δ {e1}: meta a

letbox

Γ1; ...; Γn, &Δ ⊢ e1: meta a
Γ1; ...; Γn; Δ, Δ', x: a ⊢ e2: b
------------------------------------------------ (□-elim)
Γ1; ...; Γn; Δ, Δ' ⊢ letbox x on Δ = e1 in e2: b

letbox-T

Γ1; ...; Γn, &Δ ⊢ e1: meta a
Γ1; ...; Γn, Δ, Δ', x: a ⊢ e2: b
-------------------------------------------------- (□-elim-T)
Γ1; ...; Γn, Δ, Δ' ⊢ letbox-T x on Δ = e1 in e2: b