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

IndPrinciples #32

Merged
merged 5 commits into from
Oct 30, 2017
Merged

IndPrinciples #32

merged 5 commits into from
Oct 30, 2017

Conversation

clayrat
Copy link
Collaborator

@clayrat clayrat commented Jul 25, 2017

Gah, yet another seemingly useless chapter. Not even sure I want to waste more time formatting this, given that it probably needs to be completely rewritten or dropped altogether. Thoughts?

@clayrat clayrat requested a review from yurrriq July 25, 2017 18:49
@clayrat
Copy link
Collaborator Author

clayrat commented Jul 26, 2017

So, AFAIU induction principles are subsumed/made obsolete by dependent pattern matching. We could try salvaging some examples/theory to add to the potential Tactics -> PatternMatching rewrite, but this should probably be done by someone who actually knows how these things work internally in Idris. Plus, again, the second part talks about IndProp-ish things, so it would result in sequence breaking.

@yurrriq
Copy link
Collaborator

yurrriq commented Aug 3, 2017

Is this complete, if not useless?

@clayrat
Copy link
Collaborator Author

clayrat commented Aug 3, 2017

No, I've only formatted ~1/3 and got frustrated. Maybe I'll have another look soon.

@yurrriq yurrriq added this to the First ten chapters milestone Aug 3, 2017
@clayrat clayrat mentioned this pull request Aug 3, 2017
Open
@clayrat
Copy link
Collaborator Author

clayrat commented Aug 7, 2017

Ok, I figured I could just write out the induction principles by hand to illustrate the concept. Still not sure if Idris actually works like that internally though.

@clayrat
Copy link
Collaborator Author

clayrat commented Aug 7, 2017

This SO question looks relevant: https://stackoverflow.com/questions/30598260/function-definition-by-induction-principles-in-agda

@clayrat clayrat changed the title WIP IndPrinciples IndPrinciples Aug 8, 2017
@clayrat
Copy link
Collaborator Author

clayrat commented Aug 8, 2017

Should be ok to review.

@clayrat clayrat requested review from yurrriq and removed request for yurrriq August 13, 2017 18:04
@clayrat
Copy link
Collaborator Author

clayrat commented Aug 21, 2017

So, any chance for this to get merged? :)

@clayrat
Copy link
Collaborator Author

clayrat commented Aug 21, 2017

Resolves #42

@yurrriq
Copy link
Collaborator

yurrriq commented Aug 22, 2017 •
edited
Loading

I'm a little swamped atm and it's only gonna got worse until at least Monday. If you feel good about it, go ahead and merge. 😄

@clayrat
Copy link
Collaborator Author

clayrat commented Oct 30, 2017

Ok I think this has been hanging far too long :)

@clayrat clayrat merged commit 2936a86 into develop Oct 30, 2017
@yurrriq
Copy link
Collaborator

yurrriq commented Oct 30, 2017

🎉

@clayrat clayrat deleted the indprinciples branch August 21, 2018 13:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@yurrriq yurrriq Awaiting requested review from yurrriq

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
First ten chapters
Development

Successfully merging this pull request may close these issues.
2 participants
@clayrat @yurrriq