agda

13गर्मी

1उत्तर

ऑब्जर्वेशनल टाइप थ्योरी में पैटर्न मिलान

Towards Observational Type Theory के "5. पूर्ण ओटीटी" खंड के अंत में लेखकों ने दिखाया है कि ओटीटी में कोर्सीबल-अंडर-कन्स्ट्रक्टर इंडेक्स किए गए डेटा प्रकारों को कैसे परिभाषित किया जाए। data IFin : ℕ -

5गर्मी

2उत्तर

एग्डा

के लिए हास्केल व्युत्पन्न तंत्र मैं सोच रहा हूं कि अगर एग्डा में कुछ भी है जो हैस्केल के deriving Eq खंड जैसा दिखता है --- तो मेरे पास भी एक संबंधित प्रश्न है। उदाहरण के लिए,, data Type : Set where

5गर्मी

1उत्तर

रन टाइम

से पहले प्रकार मिटा दिए गए हैं, मुझे पता है कि हास्केल प्रकारों में हमेशा रन-टाइम से पहले मिटा दिया जाता है। Agda के मामले में क्या होता है? निर्भर समय की जानकारी रन-टाइम के माध्यम से की जाती है?

9गर्मी

1उत्तर

क्या बिना एज के एजडा कम शक्तिशाली है?

What is Axiom K? पर फॉलो-अप के रूप में, मुझे आश्चर्य है कि जब आप --without-k विकल्प के साथ एग्डा का उपयोग करते हैं तो क्या होता है। क्या परिणाम कम शक्तिशाली है? क्या यह एक अलग भाषा है या क्या पिछले सभ

6गर्मी

2उत्तर

`टी b` प्रमाणन जब` b` पहले से ही पर

मैं कुछ सरल साबित करने के लिए कोशिश कर रहा हूँ मिलान किया जाता है: open import Data.List open import Data.Nat open import Data.Bool open import Data.Bool.Properties open import Relation.Binary.Pro

5गर्मी

2उत्तर

यदि दो चीजें बराबर नहीं हैं, तो क्या वे बराबर हैं?

अगर आगाडा, या कुछ अन्य निर्भर रूप से टाइप की गई भाषा में दो मान हैं, तो आप साबित कर सकते हैं कि v₁v₂ के बराबर नहीं है, क्या आप v₁v₂ के बराबर साबित कर सकते हैं? जैसे, ((v₁ ≡ v₂ → ⊥) → ⊥) → v₁ ≡ v₂ के प

6गर्मी

1उत्तर

Agda के Coinduction को समझने में समस्या

मैं निम्नलिखित paper की धारा 4 में प्रस्तुत समानांतर प्रीपेप्टिव शेड्यूलिंग के साथ आईएमपी भाषा के लिए एक कार्यात्मक अर्थशास्त्र को कोड करने का प्रयास कर रहा हूं। मैं एग्डा 2.5.2 और मानक लाइब्रेरी 0.13

10गर्मी

1उत्तर

Agda में आकार के प्रकार क्या हैं?

Agda में आकार के प्रकार क्या हैं? मैं MiniAgda के बारे में पढ़ने के लिए कागज की कोशिश की है, लेकिन आगे बढ़ने के लिए विफल रहा है निम्नलिखित बातों की वजह से: क्यों डेटा प्रकार उनके आकार से अधिक सामान्य

5गर्मी

2उत्तर

ज्ञात पैटर्न मैच

मोटे तौर पर, मैं check : UExpr -> Maybe Expr है और मैं एक परीक्षण अवधि testTerm : UExpr कौन सा मुझे आशा है कि check होगा सफलतापूर्वक, जिसके बाद मैं जिसके परिणामस्वरूप Expr निकालने और हेरफेर करने क

5गर्मी

1उत्तर

क्या इडिस के पास एग्डा के `_` अभिव्यक्तियों के बराबर है?

निहित तर्क होने के अतिरिक्त, एग्डा आपको एक स्पष्ट तर्क के मूल्य को छोड़ने और इसे _ वर्ण द्वारा दर्शाए गए मेटाएरिएबल के साथ प्रतिस्थापित करने देता है, जिसका मान तत्काल संकल्प के समान प्रक्रिया के माध्य