Russoul/Nova

Get rid of nameful meta-context in favour of a nameless one.

Opened this issue · 0 comments

We use nameful meta-context because when introducing a new name to a nameless one all terms written against the initial meta-context get invalidated in the extended one. Very error prone! We could incorporate a syntax for a StateT monad that would automatically reindex the environment against the extended meta-context. That would be an extension of Idris2 syntax though!