इसाबेल / एचओएल में "द" सिंटैक्स का उपयोग कैसे करें?

Question

मैं THEइसाबेल / एचओएल (2020) में वाक्य रचना का उपयोग करने का तरीका जानने की कोशिश कर रहा हूं । ट्यूटोरियल main.pdf में, है:

The basic logic: x = y, True, False, ¬ P, P ∧ Q, P ∨ Q, P −→ Q, ∀ x. P,
∃ x. P, ∃!x. P, THE x. P.

मैं समझ सकता हूं कि दूसरों का क्या मतलब है, लेकिन आखिरी नहीं "द एक्स। पी"। मेरा सबसे अच्छा अनुमान है "शायद (शायद अद्वितीय) एक्स जो संपत्ति पी को संतुष्ट करता है"। इसलिए मैंने निम्नानुसार एक खिलौना लेम्मा बताने की कोशिश की:

lemma "0 = THE x::nat. (x ≥ 0 ∧ x ≤ 0)"

, जिसका अर्थ है कि x जो कि ge और le दोनों है, 0 है।

लेकिन मुझे "द" शब्द पर एक हाइलाइट के साथ इसाबेल / जेएडिट में एक त्रुटि मिलती है।

मैंने इसाबेल और "THE" कीवर्ड के साथ खोज करने की कोशिश की, लेकिन जाहिर है कि खोज इंजन द्वारा "THE" शब्द को अनदेखा किया गया है। इसलिए यहां सवाल।

क्या कोई "द" वाक्यविन्यास के अर्थ और उपयोग की व्याख्या करने में मदद कर सकता है, उम्मीद है कि यहाँ उदाहरण के साथ?

Answer 1

आपको अधिक कोष्ठक की आवश्यकता है।

lemma "0 = (THE x::nat. (x ≥ 0 ∧ x ≤ 0))"
  (*the proof*)
  using theI[of ‹λx::nat. (x ≥ 0 ∧ x ≤ 0)› 0]
  by auto

कुछ (सम्मान।) हिल्बर्ट के एप्सिलॉन ऑपरेटर का एक प्रकार है जो एक निश्चित संपत्ति का सम्मान करता है (एक) तत्व देता है। यदि कोई नहीं (कोई भी या एक से अधिक) मौजूद नहीं है, तो एक अंडरसिज्ड तत्व वापस आ जाता है।

SOME और THE निष्पादन योग्य नहीं हैं। वे शुरुआती लोगों के लिए शायद ही कभी उपयोगी होते हैं।