Get rid of nameful meta-context in favour of a nameless one.
Opened this issue · 0 comments
Russoul commented
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!