New blog post, "Logic Proofs with Coq, Agda, and Idris": https://blog.cppcabrera.com/posts/48-logic-proofs-with-agda-coq-idris.html … Props as Types in action, with code and thoughts.
-
-
Replying to @queertypes
@cppcabrera The strange proof you've encountered isn't a bug in Idris, but in your definition of Or: "data Or a b = Inl a | Inr a"
1 reply 1 retweet 6 likes -
Replying to @edwinbrady
@edwinbrady Thank you! Code review is so important. I'll go fix things up in my post.1 reply 0 retweets 1 like
Replying to @queertypes
@cppcabrera I spent a few minutes trying to work out what was going on and was very puzzled until I thought to look there :)
3:10 PM - 17 Jun 2015
0 replies
0 retweets
3 likes
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.