6
में टुपल के लिए लेट-डिस्ट्रक्ट का उपयोग करने में विफलता मैं Coq के लिए एक नया उपयोगकर्ता हूं। मैंने कुछ कार्यों को परिभाषित किया है:कोक
Definition p (a : nat) := (a + 1, a + 2, a + 3).
Definition q :=
let (s, r, t) := p 1 in
s + r + t.
Definition q' :=
match p 1 with
| (s, r, t) => s + r + t
end.
मैं पी के परिणाम को टुपल प्रतिनिधित्व में नष्ट करने की कोशिश कर रहा हूं। हालांकि coqc q पर शिकायत करता है:
Error: Destructing let on this type expects 2 variables.
जबकि q 'संकलन पास कर सकता है। यदि मैं एक जोड़ी (ए + 1, ए + 2) वापस करने के लिए पी बदलता हूं, तो संबंधित क्यू और क्यू 'दोनों ठीक काम करते हैं।
क्यों चलो विनाश केवल जोड़ी की अनुमति देता है? या मैंने वाक्यविन्यास में कोई त्रुटि की है? मैंने कोक मैनुअल के साथ जांच की है लेकिन कोई सुराग नहीं मिला है।
धन्यवाद!
धन्यवाद! तो 3 सदस्यीय ट्यूपल को जोड़ी के पहले सदस्य पर फिर से नष्ट करने के रूप में माना जाना चाहिए, तो मुझे 'उद्धरण' का उपयोग करना होगा? – xywang
हाँ, यही वह है! –