New
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.

6 questions
Filter by
Sorted by
Tagged with
13 views

### Idris Leap Year Test Implementation

I've built the following isLeapYear function in Idris: ...
205 views

### 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: ...
• 5,906
451 views

### 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 ...
• 233
68 views

### 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 ...
• 193
279 views

### 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 ...
• 291