search

exercism / idris

Exercism exercises in Idris.
https://exercism.org/tracks/idris
MIT License
32 stars 18 forks source link

Add Leap exercise #13

Closed stevejb71 closed 7 years ago

stevejb71 commented 7 years ago

WIP (having trouble running make test for both this and the HelloWorld exercise, so untested).

yurrriq commented 7 years ago

Thanks. I've got some ideas in the works for testing. For now, please name the example file example.idr in exercises/leap-year or whatever. You may have already. I'm commenting before reading.

yurrriq commented 7 years ago

Can we rename leap to isLeap? I'd like to prefix Boolean predicates with is, I think.

yurrriq commented 7 years ago

Also, I think we should add a src/Leap.idr file with a skeleton module, something like:

module Leap

isLeap : Int -> Bool
isLeap year = ?isLeap_rhs

We should do something similar (and uniform) for all exercises, I think.

yurrriq commented 7 years ago

I've got a nice, reproducible, CI-friendly testing strategy worked out on tdd-with-idris and plan to adapt something similar for xidris.

Re: skeleton modules and holes, see code/discussion on idris-hackers/software-foundations.

stevejb71 commented 7 years ago

I agree with adding a type hole, at least for the initial few exercises. Also changed leap to isLeap, and fixed a mistake in one of the tests.

yurrriq commented 7 years ago

This looks good. Thanks!