search

idris-hackers / software-foundations

Software Foundations in Idris
https://idris-hackers.github.io/software-foundations
MIT License
452 stars 34 forks source link

IndPrinciples #32

Closed clayrat closed 7 years ago

clayrat commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

Is this complete, if not useless?

clayrat commented 7 years ago

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

clayrat commented 7 years ago

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 commented 7 years ago

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

clayrat commented 7 years ago

Should be ok to review.

clayrat commented 7 years ago

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

clayrat commented 7 years ago

Resolves https://github.com/idris-hackers/software-foundations/issues/42

yurrriq commented 7 years ago

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. :smile:

clayrat commented 7 years ago

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

yurrriq commented 7 years ago

:tada: