Tests at compile time? about idris HOT 6 CLOSED

I'd prefer to use idris-testing.

from idris.

I'm not sure but I think this way of "testing" (it's rather the compiler ensuring, with the help of types, that the program is correct) doesn't apply to all problems. For example, in the "hello world" exercise, it's not obvious to me how to do something similar. (Maybe by changing the types?)

from idris.

I'll have a try with hello-world.
I like it because

• dependent types are a key feature of Idris which this highlights
• does not need any dependencies.

from idris.

For the leap year and hello world exercises this works ok, but in general I'm opposed to it. If you wanted instead to prove theorems about properties of a given exercise, that would be ok.

from idris.

@yurrriq I agree. It would make sense to keep hello world as simple as can be -- for getting your feet wet with the exercism CLI, testing of Idris, ... -- and there's nothing keeping you from revisiting hello world (or leap year) to look into advanced features of Idris. This would then be another exercise, though. (I realise that this is not exactly what you proposed, but rather a slight variation of it. 😉 )

from idris.

Closing this since we're going with the unit testing approach.

from idris.