Skip to main content
Stack Overflow Jobs powered by Indeed: A job site that puts thousands of tech jobs at your fingertips (U.S. only). Search jobs

Questions tagged [idris]

Idris is a general purpose pure functional programming language with dependent types.

Filter by
Sorted by
Tagged with
0 votes
0 answers

Idris Leap Year Test Implementation

I've built the following isLeapYear function in Idris: ...
Onorio Catenacci's user avatar
6 votes
1 answer

Proof that two lines intersect each other at precisely one point in Idris

I recently attempted to prove that given two lines, they intersect at one and only one point in Idris. Here is what I came up with: ...
Dair's user avatar
  • 5,906
13 votes
1 answer

Proving that merging two sorted lists produces a sorted list

I'm just starting to learn using both dependent types and proof assistants, and as an exercise I'm trying to write a provably correct merge sort. As a first step, I'm writing a function that merges ...
0xd34df00d's user avatar
2 votes
1 answer

Axiomatic proofs of natural addition properties, in Idris

I'm a seasoned programmer in a variety of languages (including Haskell and some ML dialects), but i'm a complete dilettante when it comes to formal logic. I've very briefly looked at Coq, and now i'm ...
b0fh's user avatar
  • 193
6 votes
0 answers

Idris - Bowling scoring

Having read the great Type Driven Development in Idris book, I started fiddling with an implementation for a Bowling scoring system in Idris. My initial goal was to model the score with types and ...
theimowski's user avatar
13 votes
2 answers

Vending Machine in Idris

Type Driven Development with Idris demonstrates how Idris can be used to build a Finite State Machine for a vending machine. Please critique my implementation. I'm new to dependent types, so I'm not ...
Kevin Meredith's user avatar