2
votes
Accepted
Proof that two lines intersect each other at precisely one point in Idris
It still may be far from perfect, but I asked a question on Stackoverflow related to this, and received an excellent answer from xash.
I have attempted to cure my Boolean blindness. If I understand ...
- 6,008
2
votes
Accepted
Proving that merging two sorted lists produces a sorted list
and welcome to Code Review.
I'll be perfectly upfront here: your post 8 days ago was the first I had ever heard of idris. I was hoping that someone who knew it, or even knew a bit more Haskell, might ...
- 6,016
1
vote
Vending Machine in Idris
You can index your Machine type by a (type-level) state to statically disallow certain operations. For example, suppose you only want to allow filling the machine ...
- 202
Only top scored, non community-wiki answers of a minimum length are eligible