इडिस: क्या "साथ" के बजाय "केस" का उपयोग करने के लिए "साथ" का उपयोग करके सभी कार्यों को फिर से लिखना संभव है? यदि नहीं, तो क्या आप एक काउंटर उदाहरण दे सकते हैं?

Question

इडिस में, "साथ" के बजाय "केस" का उपयोग करने के लिए "with" का उपयोग करके सभी कार्यों को फिर से लिखना संभव है?

यदि नहीं, तो क्या आप काउंटर उदाहरण दे सकते हैं?

Answer 1

संभव नहीं है। जब आप with के साथ पैटर्न मिलान करते हैं, तो संदर्भ में प्रकार मिलान किए गए कन्स्ट्रक्टर से निकाली गई जानकारी के साथ अपडेट किए जाते हैं। case ऐसे अद्यतन का कारण नहीं है।

उदाहरण के लिए, with साथ नहीं बल्कि case के साथ निम्न काम करता है:

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