EG
Простой пример на идрисе из книги:
Круто! Но, я тут подумал — я хочу матчить не по булу, а по инту. У инта тоже фиксированный набор значений, почему бы этому не сработать?
Упс.
my_type : Bool -> Type
my_type True = Int
my_type False = String
my_func : (x : Bool) -> (my_type x)
my_func True = 42
my_func False = "forty two"
Круто! Но, я тут подумал — я хочу матчить не по булу, а по инту. У инта тоже фиксированный набор значений, почему бы этому не сработать?
my_type : Int -> Type
my_type 0 = Int
my_type _ = String
my_func : (x : Int) -> (my_type x)
my_func 0 = 42
my_func _ = "forty two"
Упс.