agda

4熱度

1回答

我寫了一個Agda函數applyPrefix將固定大小的向量函數應用於更長的向量的初始部分，其中向量大小m,n和k可能保持隱含。這裏用一個輔助功能split的定義一起： split : ∀ {A m n} → Vec A (n + m) → (Vec A n) × (Vec A m) split {_} {_} {zero} xs = ([] , xs) split {_} {_} {suc

3熱度

1回答

類型錯誤試圖模式匹配的東西，應該是荒謬反正

在類型檢查的簡單類型的演算中間的時候，我有這樣的： check Γ (lam τ′ E) (τ₁ ↣ τ₂) with τ′ T≟ τ₁ check Γ (lam τ′ E) (τ₁ ↣ τ₂) | no ¬p = no lem where lem : ¬ Γ ⊢ lam τ′ E ∷ (τ₁ ↣ τ₂) lem t = {!!} 類型的孔是當然，⊥。我希望通過

9熱度

1回答

Agda：Conor的堆棧示例的運行函數

在ICFP 2012上，Conor McBride發表了關於「Agda好奇？」的主題演講。它具有一個小型堆棧機器的實現。的視頻在YouTube上： http://www.youtube.com/watch?v=XGyJ519RY6Y 的代碼在網上太： http://personal.cis.strath.ac.uk/conor.mcbride/ICFP12Code.tgz 我想知道5部分（即「

3熱度

2回答

局部進口數據類型的衝突定義一個，甚至改名

用下面的阿格達代碼的時候，我在A₂得到的B定義的錯誤： module Whatever where module A₁ where data B : Set where module A₂ where open A₁ renaming (B to B₁) data B : Set where 的錯誤信息是： Duplicate definition of

5熱度

1回答

Agda：具有相同長度的一對向量

在Agda中，如何定義一對必須具有相同長度的向量？ -- my first try, but need to have 'n' implicitly b : ∀ (n : ℕ) → Σ (Vec ℕ n) (λ _ → Vec ℕ n) b 2 = (1 ∷ 2 ∷ []) , (3 ∷ 4 ∷ []) b 3 = (1 ∷ 2 ∷ 3 ∷ []) , (4 ∷ 5 ∷ 6 ∷ []) b

3熱度

1回答

是什麼infixr在阿格達意思？

Prp : Set₁ Prp = Set data _∧_ (P Q : Prp) : Prp where ∧-intro : P -> Q -> P ∧ Q infixr 2 _∧_ data _∨_ (P Q : Prp) : Prp where ∨-intro₁ : P -> P ∨ Q ∨-intro₂ : Q -> P ∨ Q infix

1熱度

2回答

_∷«_»_：（X：ℕ） - >分≤X - > MinList X - > MinList分鐘

data MinList (min : ℕ) : Set where [] : MinList min _∷⟪_⟫_ : (x : ℕ) -> min ≤ x -> MinList x -> MinList min 任何理想是什麼< < >>是什麼意思？或什麼的 _∷⟪_⟫_ : (x : ℕ) -> min ≤ x -> MinList x -> MinList min

25熱度

1回答

在排列

的表示，我想有一個感應式來描述置換及其對某些容器行動。清楚的是，取決於這種類型的描述，算法的定義複雜性（按其長度）（計算組合或逆，分解成不相交的週期等）將會變化。考慮勒柯克下面的定義。我相信這是萊默代碼形式化： Inductive Permutation : nat -> Set := | nil : Permutation 0 | cons : forall (n k : nat), Pe

12熱度

2回答

Haskell的箭級在阿格達和 - >在阿格達

我有兩個密切相關的問題：首先，如何能在Haskell的箭類建模/在阿格達代表？ class Arrow a where arr :: (b -> c) -> a b c (>>>) :: a b c -> a c d -> a b d first :: a b c -> a (b,d) (c,d) second :: a b c -> a (d,b

10熱度

1回答

Agda中的類型層次結構

我想知道如何在Agda中使用類型層次結構。假設我定義一組類型X： X : Set ，然後進行構建的感應型 data Y : X -> Set where 什麼是X -> Set類型？它是設置還是類型？謝謝！