not in idris, because it would force you to do that check manually and pass in the evidence as proof. it has a bunch of tools to help you do this.. namely lift

not in idris, because it would force you to do that check manually and pass in the evidence as proof. it has a bunch of tools to help you do this.. namely lifting values into types with 'dependent pairs'. idris doesnt automagically calculate everything for you, but makes sure at compile time, that you provide evidence at run time for the things you have asserted in the types. it makes more sense after going through some of the tutorials and books.