Comparison of samples by type in Idris

Perhaps this is elementary, but I do not understand why the following function answers 1 for fnc Nat , as well as for fnc Integer , which is not even included as a template.

fnc : Type -> Integer
fnc Bool = 1
fnc Nat = 2
+3
source share
1 answer

You cannot match matching by type, and you shouldn't. When I compile the code, I get the following error:

warning - Unreachable case: fnc Nat

This has already been discussed previously:

UPDATE:

Finally, I found a more relevant question with the answer:

Why is typecase a bad thing?

+2
source

Source: https://habr.com/ru/post/1683561/


All Articles