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.

Sign up for GitHub

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

Jump to bottom

Reimplement sort system #866

Closed
1 of 5 tasks
ice1000 opened this issue Dec 29, 2022 · 2 comments · Fixed by #874 or #875
Closed
1 of 5 tasks

Reimplement sort system #866

ice1000 opened this issue Dec 29, 2022 · 2 comments · Fixed by #874 or #875
Assignees
@ice1000
Labels
prop Universe of propositions

Comments

@ice1000
Copy link
Member

ice1000 commented Dec 29, 2022 •
edited
Loading

Taken from #507

Update (2023/2/17): I now believe that irrelevance as a universe is very weird. I would like to remove this feature and add irrelevance modality later.

  • tyck rules for top level defs
  • [x] Prop tyck rules
  • more Set tyck rules
  • disallow data to live in ISet
  • [ ] non-Prop metas
  • [x] irrelevance of propositions (that, if A : Prop and a b : A, then a = b definitionally)
  • pi domain checks
  • [x] pattern matching restrictions
  • Paths should be restricted to Type
@ice1000 ice1000 added the prop Universe of propositions label Dec 29, 2022
@ice1000 ice1000 self-assigned this Dec 29, 2022
@ice1000 ice1000 mentioned this issue Dec 29, 2022
Closed
8 tasks
@ice1000
Copy link
Member Author

ice1000 commented Jan 6, 2023

Ref: #449

@ice1000 ice1000 linked a pull request Jan 6, 2023 that will close this issue
Reimplement sort system: step 1 #874
Merged
@ice1000 ice1000 mentioned this issue Jan 6, 2023
Merged
bors bot added a commit that referenced this issue Jan 7, 2023
@bors @ice1000
merge: #875
34f1ef1 
875: Irrelevance of `Prop` WIP r=ice1000 a=ice1000

#866 

Co-authored-by: ice1000 <ice1000kotlin@foxmail.com>
@ice1000 ice1000 linked a pull request Jan 7, 2023 that will close this issue
Irrelevance of Prop WIP #875
Merged
@ice1000
Copy link
Member Author

ice1000 commented May 18, 2024

We temporarily give up Prop due to its complication

@ice1000 ice1000 closed this as completed May 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ice1000 ice1000

Labels
prop Universe of propositions
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Reimplement sort system: step 1 aya-prover/aya-dev
Irrelevance of Prop WIP aya-prover/aya-dev
1 participant
@ice1000