Generic:一个用于在Agda中进行通用编程的库

通用的 这是一个用于在Agda中进行通用编程的库。 该库已经过Agda-2.6.1和Agda-2.6.1.2的测试，可能不适用于其他版本的Agda。 快速品尝 得出向量的可判定相等性： open import Data.Vec using (Vec) renaming ([] to []ᵥ; _∷_ to _∷ᵥ_) instance VecEq : ∀ {n α} {A : Set α} {{aEq : Eq A}} -> Eq (Vec A n) unquoteDef VecEq = deriveEqTo VecEq (quote Vec) xs : Vec ℕ 3 xs = 2 ∷ᵥ 4 ∷ᵥ 1 ∷ᵥ []ᵥ test₁ : xs ≟ xs ≡ yes refl test₁ = refl test₂ : xs ≟ (2 ∷ᵥ 4 ∷ᵥ 2 ∷ᵥ []ᵥ) ≡ no _ tes