Как сделать базовое сопоставление с формальными параметрами (привязка значений) в Idris? - PullRequest
Новая
       12

Как сделать базовое сопоставление с формальными параметрами (привязка значений) в Idris?

0 голосов
/ 30 мая 2018

Когда я пытаюсь это сделать в Idris, 

contrived : (List a, Char, (Int, Double), String, Bool) -> Bool
contrived   ([]    ,  'b',  (1,   2.0),   "hi" , True) = False
contrived    (a,  b,  c,   d,  e) = True

я получаю сообщение об ошибке Can't infer argument a to contrived, Can't infer argument a to List, Can't infer argument a to [].Но, глядя на книгу Мэннинга, я не вижу очевидных синтаксических проблем с моим подходом.

1 Ответ

0 голосов
/ 30 мая 2018

вы получаете сообщение об ошибке, так как Idris хотел бы узнать, какой тип a (или, скорее, [], когда вы вызываете функцию в REPL. Вы можете указать эту неявную информацию следующим образом: 

contrived {a = Nat} ([],  'b',  (1, 2.0), "hi" , True)
> False

Или вот так: 

contrived (the (List Nat) [],  'b',  (1, 2.0), "hi" , True)
> False

В true программе, которая не требуется: 

EmptyList: List Nat
EmptyList = []

testCase: contrived (EmptyList, 'b', (1, 2.0), "hi", True) = False
testCase = Refl
...