如果我试图证明Nat和Bool在Agda中不相等: open import Data.Natopen import Data.Emptynoteq () 我得到了错误: Failed to solve the followingconstraints:
Is empty: ℕ ≡ Bool 我知道不可能对
在Agda中,似乎不可能显示∀ {A : Set} (f : ⊥ → A) → f ≡ λ ()。然而,看似相似的术语∀ {A : Set} (f : ⊤ → A) → f ≡ λ _ → f tt可以被refl证明。以后可以用来证明⊤的一种可扩展性。ext⊤ : ∀ {A : Set} (f g : ⊤ → A) (H : ∀ x → f x ≡ g x) → f ≡ g
认为,解释可能是考虑了不同的类型理论模型。f ≡ λ ()不应该是某种形式<e
TL;DR:在Agda中,给定a : A和proof : A == B,我能获得一个元素a : B吗?在我不断尝试学习Agda的过程中,我创建了以下Prime : nat -> Set数据类型,这是一个自然的原始性的见证。-> divides i p -> i <N p -> zero <N i -> i == (succ zero)