में सिर मैं एग्डा में एक साधारण लेम्मा साबित करने की कोशिश कर रहा हूं, जो मुझे लगता है कि सच है।दिखा रहा है (सिर। Init) = अंगडा
एक वेक्टर दो से अधिक तत्वों,
init
लेने के बाद अपनेhead
लेने है, तो इसकीhead
तुरंत लेने के समान है।
मैं इसे तैयार की इस प्रकार है:
lem-headInit : ∀{l} (xs : Vec ℕ (suc (suc l)))
-> head (init xs) ≡ head xs
lem-headInit (x ∷ xs) = ?
कौन सा मुझे देता है;
.l : ℕ
x : ℕ
xs : Vec ℕ (suc .l)
------------------------------
Goal: head (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs)) ≡ x
एक प्रतिक्रिया के रूप में।
मैं पूरी तरह से समझ नहीं पा रहा हूं कि (init (x ∷ xs) | (initLast (x ∷ xs) | initLast xs))
घटक कैसे पढ़ा जाए। मुझे लगता है कि मेरे प्रश्न हैं; क्या यह संभव है, उस शब्द का अर्थ और कैसे अर्थ है।
बहुत धन्यवाद।