Question  Automatic detection of domain for dependent type function in Idris 

Answers  1  
Added at  20161225 16:12  
Tags  
Question 
Idris language tutorial has simple and understandable example of the idea of Dependent Types: http://docs.idrislang.org/en/latest/tutorial/typesfuns.html#firstclasstypes Here is the code:
I decided to spend more time on this example. What bothers me in Of course, I understand, this is not possible in general case. Such compiler tricks require my function So I started with next implementation: I just made
Well, it doesn't really solve my problem because I still need to call this function in the next way:
But I read in tutorial about
And it works for lists!
But doesn't work for single value :(
Can someone explain is it actually possible to achieve my goal in such injective function usages currently? I watched this short video about proving something is injective: https://www.youtube.com/watch?v=7Ml8u7DFgAk But I don't understand how I can use such proofs in my example. If this is not possible what is the best way to write such functions? 

Answers 


Source  Show 