@edwinbrady weird question due to me learning Coq: does Idris unify the Proofs and Computational types in the same hierarchy?
@Lenary Yes. Sometimes you want to compute over proofs, and we have more aggressive erasure.
-
-
@edwinbrady is there a test of this I could see to try and make sense of it? -
@Lenary What sort of test are you after? I just knocked up https://gist.github.com/edwinb/8551794 - 1 more reply
New conversation -
-
-
@edwinbrady also, i may now be imagining a very angry rubber. Whelp.Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
@edwinbrady Time we nailed this properly. I wrote this chunk of stuff. Not quite our beer mat. https://personal.cis.strath.ac.uk/conor.mcbride/pub/phtt.pdf … Want in?@Lenary -
@pigworker@edwinbrady I probably won't understand this. Still doing really basic stuff with Coq, but interested by several ideas.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.