Skip to content

Make use of new features in Agda 2.6.0 #527

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

Closed
4 of 5 tasks
gallais opened this issue Nov 9, 2018 · 6 comments
Closed
4 of 5 tasks

Make use of new features in Agda 2.6.0 #527

gallais opened this issue Nov 9, 2018 · 6 comments
Milestone

Comments

@gallais
Copy link
Member

gallais commented Nov 9, 2018

We could either wait for it to be released or resurrect experimental.

  • Check the library with the --safe flag on
  • Use primEraseEquality (in Agda.Builtin.Equality.Erase)
  • Use generalisation
  • Use smarter coverage checker
  • The warnings for missing fixities should now work properly
@MatthewDaggitt
Copy link
Contributor

Given the problems we've had in the past, my gut feeling is that we should hold off for a while until 2.6.0 has a more firm release date? Unless I've missed something and it's coming out soon?

@UlfNorell
Copy link
Member

We're aiming for a Christmas release, but as usual, no promises.

@MatthewDaggitt
Copy link
Contributor

MatthewDaggitt commented Nov 9, 2018

Hmm in that case we probably should get on it. Feel free to bring the experimental branch up-to-date.

@gallais gallais added this to the v1.0 milestone Mar 1, 2019
@gallais gallais modified the milestones: v1.0, v1.1 Mar 10, 2019
@MatthewDaggitt
Copy link
Contributor

@gallais what does the last point on the list refer to?

@gallais
Copy link
Member Author

gallais commented May 13, 2019

It refers to #207

@MatthewDaggitt
Copy link
Contributor

It refers to #207

Okay thanks. Closing this as it has its own issue.

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

No branches or pull requests

3 participants