İdris: o "ile" "harf" kullanmak yerine, söz konusu "ile" kullanarak tüm fonksiyonlarını yeniden yazmak mümkün mü? Yoksa, karşı bir örnek verebilir misiniz? Idris yılında

Question

, bunun yerine "ile" nin "case" kullanımı "with" seçeneğini kullanarak tüm fonksiyonları yeniden yazmak mümkün mü? Değilse

, bir karşı örnek verebilir misiniz?

Answer 1

mümkün değil. with ile size desen maç bağlam içinde tipleri eşleşti yapıcı çıkarılan bilgilerle güncellenir zaman. case böyle bir güncelleştirmeye neden olmaz. with ile değil case ile Örnek olarak

aşağıdaki çalışır: cevap Andras için

import Data.So 

-- here (n == 10) in the goal type is rewritten to True or False 
-- after the match 
maybeTen : (n : Nat) -> Maybe (So (n == 10)) 
maybeTen n with (n == 10) 
    maybeTen n | False = Nothing 
    maybeTen n | True = Just Oh 

-- Here the context knows nothing about the result of (n == 10) 
-- after the "case" match, so we can't fill in the rhs 
maybeTen' : (n : Nat) -> Maybe (So (n == 10)) 
maybeTen' n = case (n == 10) of 
    True => ?a 
    False => ?b