search

idris-hackers / software-foundations

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

Logic #18

Closed clayrat closed 7 years ago

clayrat commented 7 years ago

Not sure how to deal with the Setoids part here, there seem to exist some 3rd party formulations for them, e.g. https://github.com/danilkolikov/setoids https://github.com/qradimir/tt-homework/blob/master/src/main/idris/Setoid.idr https://github.com/artemohanjanyan/university/blob/master/4_term/types/idris/Setoid.idr https://github.com/shd/tt2016/blob/master/diaconescu.idr https://github.com/eadm/rational-setoid/blob/master/Setoid.idr but how to make them work with the rewriting machinery?

david-christiansen commented 7 years ago

We don't currently have a good way to do rewriting in setoids. It would require a compiler extension or some Elab magic.

clayrat commented 7 years ago

I feel like Logic is good enough.

yurrriq commented 7 years ago

N.B. Not every one of my review comments requires any action.

clayrat commented 7 years ago

Addressed most of them.

yurrriq commented 7 years ago

This looks great. Thanks for putting the todos in the file, too.