agda

0熱度

2回答

我想證明agda的交換屬性。我試圖探索標準庫，但有很多複雜的東西，我無法理解。我試圖以這種方式 - comm : (a b : Q) -> (a + b) === (b + a) 這裏的問題是不是在圖書館過Q定義+。我們不能證明這一點，沒有定義+ Q. 請指導我。

1熱度

1回答

如何在agda中添加兩個理性？

如何添加兩個理性..我正在嘗試這個，但這是不正確的。因爲我無法證明這個coprime部分。 open import Data.Rational open import Data.Integer open import Data.Nat _add_ : ℚ -> ℚ -> ℚ x add y = (nx Data.Integer.* dy Data.Integer.+ dx Data.In

2熱度

1回答

在應用程序中使用SUBST將螺釘向上結果

我有以下類型的定義的類型： insert : ∀ {n} → (i : Fin (suc n)) → ∀ t → Env n → Env (suc n) weaken : ∀ {t t₀ n} {Γ : Env n} → (i : Fin (suc n)) → (e : Γ ⊢ t₀) → (insert i t Γ) ⊢ t₀ 鑑於環境Γ : Env n和Γ′ : Env n′，並在第二個

11熱度

1回答

建模阿格達

的ST單子最近的這次SO question促使我寫在Haskell，略加修改的ST單子，其中你可以看到下面的不安全和純仿真： {-# LANGUAGE DeriveFunctor, GeneralizedNewtypeDeriving, RankNTypes #-} import Control.Monad.Trans.State import GHC.Prim (Any) import

23熱度

1回答

所以：有什麼意義？

So類型的預期用途是什麼？音譯成阿格達： data So : Bool → Set where oh : So true So升降機布爾命題到邏輯一。 Oury和Swierstra的介紹性文章The Power of Pi給出了一個由表格列索引的關係代數的例子。以兩個表的產品需要，他們有不同的列，爲此，他們使用So： Schema = List (String × U) -- U i

2熱度

2回答

如何獲取Data.AVL.Tree中的值列表？

我能夠輕易獲得密鑰列表如下： open import Relation.Binary open import Relation.Binary.PropositionalEquality using (_≡_) module AVL-Tree-Functions { k v ℓ } { Key : Set k } (Value : Key → Set v) { _

2熱度

1回答

實例搜索限制

實例參數機制在舊的paper和at the Agda wiki中描述。有沒有一些值得注意的事實，這些來源沒有提到？實例搜索有什麼限制？

0熱度

1回答

Agda統一列表

我正在做一個證明正則表達式的一些屬性的項目。這裏是我的代碼 ⇨這裏單元導出部分，Regexp ⇨ word表示正則表達式可以推導出一個字 Σ : Set Σ* : List Σ 下面定義的情況下，當串聯e₁ ∙ e₂可以得到一個字w如果e₁ ⇨ w₁，e₂ ⇨ w₂和w ≡ w₁ ++ w₂ data _⇨_ : RegExp Σ → Σ* → Set where con : {e₁ e

2熱度

1回答

意外的宇宙級

這裏是一個類似於在Data.List.All一個定義： open import Data.Vec data All {α π} {A : Set α} (P : A -> Set π) : ∀ {n} -> Vec A n -> Set π where []ₐ : All P [] _∷ₐ_ : ∀ {n x} {xs : Vec A n} -> P x -> All P

3熱度

1回答

在伊德里斯

恢復型比方說，我有一個數據類型： data Term : Type -> Type where Id : Term (a -> a) ... App : Term (a -> b) -> Term a -> Term b 有了一個證明事情是App： data So : Bool -> Type where Oh : So True isApp :