Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
Russoul opened this issue Dec 27, 2023 · 0 comments
Open

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

Russoul opened this issue Dec 27, 2023 · 0 comments

Comments

@Russoul
Copy link
Owner

Russoul commented Dec 27, 2023

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!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant