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

Make a core version of variable, check them, and introduce dependencies in stmt tycker #1220

Open
ice1000 opened this issue Dec 15, 2024 · 0 comments

Comments

@ice1000
Copy link
Member

ice1000 commented Dec 15, 2024

Right now, variable A : B cannot have inter-dependencies.

Would be nice to support

variable A : Type
variable a : A

and using a automatically introduces A.

Note that this needs to be recursive, so

variable A : Type
variable k : K
variable n : G k
variable xs : F A n

and using xs will cause everything else to be introduced.

@ice1000 ice1000 linked a pull request Jan 31, 2025 that will close this issue
@ice1000 ice1000 removed a link to a pull request Jan 31, 2025
@ice1000 ice1000 assigned ice1000 and unassigned mio-19 Feb 1, 2025
@ice1000 ice1000 changed the title Support dependent types in variable Make a core version of variable, check them, and introduce dependencies in stmt tycker Feb 1, 2025
@ice1000 ice1000 linked a pull request Feb 1, 2025 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants