agda

0熱度

2回答

使用agda標準庫（v13）如何填充下一個孔？ $ cat foo.aga open import Data.List using (List ; [] ; _∷_ ; _++_ ; [_]) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; trans; sym) p

2熱度

1回答

證明語言連接在Agda中是關聯的

我是Agda語言的新手，我正在使用Agda正式語言。當證明語言連接是關聯時，我遇到了一些問題。該證明將是黃色突出顯示爲阿格達不能在下面的代碼中找到了「++副教授」的話來說： LangAssoc : ∀{Σ}{l1 l2 l3 : Language Σ}{w : Word Σ} → (LangConc l1 (LangConc l2 l3)) w → (LangConc (LangConc l1

1熱度

1回答

從Coq到Agda的移植（簡單型）lambda微積分術語飽和證明

我試圖從Software Foundations, vol. 2端口msubst_R Agda。我試圖通過對術語使用類型化表示來避免繁重的工作。下面是我的一切到msubst_R;我認爲以下一切都很好，但這是有問題的部分。 open import Data.Nat open import Relation.Binary.PropositionalEquality hiding (subst) o

1熱度

1回答

如果在CoC上不可能有O（1）pred，那麼爲什麼這會起作用？

我一直認爲已經證明pred不能在任何數據類型編碼的微積分結構中以恆定時間表示。現在，考慮到這一點編碼NATS： S0 : ∀ (r : *) . (r -> r) -> r -> r S0 = λ s z . z S1 : ∀ (r : *) (((∀ (r : *) . (r -> r) -> r -> r) -> a) -> (a -> a))) S1 = λ s z . (s (λ

0熱度

2回答

證明n次偶數在Agda中產生偶數

我試圖在Agda 中定義1..n∈ℕ的和爲n *（n + 1）/ 2，並且需要證明n * （n + 1）就是這樣。證明非常簡單，但似乎有一個概念我不明白，因爲我是Agda的新手（雖然對數學和哈斯克爾都不熟悉），並從http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf 中得知它（指向更高級的教程比歡迎！）。 open import

1熱度

1回答

如何處理Agda不確定是否在`with`語句中生成構造函數？

我有以下代碼： open import Data.Nat open import Agda.Builtin.Char open import Data.Maybe digit' : ℕ → Maybe ℕ digit' n with compare n (primCharToNat '9') ... | greater _ _ = nothing ... | _ = ? digi

1熱度

1回答

添加實例參數如何幫助實例搜索？

不小心，我設法讓實例搜索成功，但我不明白爲什麼。在下面的代碼中，爲什麼test2成功，但test1失敗（未解決的metas &約束）？ ⦃ isRelation ⦄參數的添加如何幫助IsSymmetric2？我認爲它必須與某些metas得到解決，因此允許實例搜索成功，但除此之外，我很霧。有人可以闡明這裏的工作機制嗎？有一個答案here觸及我的問題（「弱點」部分），但沒有解釋如何解決方法的機制

0熱度

1回答

解析errror：Agda和其標準庫之間的版本不匹配

我正在運行預構建的Windows Agda版本2.4.2.2。在Emacs/Agda2包括Dirs我已經識別c：/agda-stdlib-0.13/src和下一級文件夾。加載一個僅由這兩行組成的模塊時，我收到一條錯誤消息。 module test1 where open import Integer 錯誤消息： C:\agda-stdlib-0.13\src\Data\Empty.agd

1熱度

1回答

Agda中可判定的等於少於n^2個案件？

我有一個編程語言AST的數據類型，我想推理一下，但AST的約有10種不同的構造函數。 data Term : Set where UnitTerm : Term VarTerm : Var -> Term ... SeqTerm : Term -> Term -> Term 我想寫一個函數，該語言的語法樹具有可判定的相等性。理論上，這很簡單：沒有太複雜的

1熱度

1回答

如何消除衝突構造函數名稱

參見stdlib中的示例Data.Maybe.Base - 所有Maybe,Any和All都有一個just構造函數。 Agda允許這些定義。如何指定使用哪一個？