Agda中数据类型的可判定相等性
Agda是一种依赖类型理论的函数式编程语言，它被广泛应用于形式化验证和证明的领域。在Agda中，数据类型的可判定相等性是一种重要的概念。
数据类型的可判定相等性是指能够确定两个给定的值是否相等的属性。在Agda中，使用_≡_或_==_等符号来表示相等性。对于两个值a和b，如果存在类型为a ≡ b的证据，则表示a和b是相等的。这个证据可以通过多种方式构造，例如使用反射、路径归纳等等。
数据类型的可判定相等性在形式化验证中非常有用，可以用来证明程序的正确性和性质。它允许我们在程序中进行精确的相等性比较，并得到严格的证明结果。
在Agda中，数据类型的可判定相等性还可以与其他类型一起使用，例如函数类型、记录类型等等。这样可以定义更复杂的数据结构和算法，并对其进行形式化验证。
在使用Agda进行编程时，可以通过使用标准库中的Relation.Binary.PropositionalEquality模块来处理数据类型的可判定相等性。这个模块提供了一些用于操作和证明相等性的函数和定理。
腾讯云的相关产品和服务与Agda中数据类型的可判定相等性可能没有直接的联系。然而，作为一个云计算专家和开发工程师，我可以推荐腾讯云的一些相关产品，供您参考：
- 腾讯云计算服务（Cloud Computing Services）：提供弹性计算、存储和网络等基础设施服务，支持云计算应用的部署和运行。
- 腾讯云人工智能服务（Artificial Intelligence Services）：包括图像识别、语音识别、自然语言处理等人工智能能力，可以与Agda中的类型和证明相结合，用于构建智能化的应用程序。
- 腾讯云数据库（Database Services）：提供关系型数据库、NoSQL数据库等多种选择，用于存储和管理数据。
- 腾讯云安全服务（Security Services）：提供云安全解决方案，包括DDoS防护、防火墙、数据加密等，保护云计算应用的安全性。
以上是一些建议和推荐的腾讯云产品和服务，供您参考。请注意，这仅是其中的一部分，腾讯云还提供其他丰富的产品和解决方案，可以根据具体需求进行选择和使用。如需了解更多详情，请参阅腾讯云官方网站（https://cloud.tencent.com/）上的相关文档和资料。
相关·内容
1回答
我在使用字符串可判断性时遇到了问题。首先，我搞不懂为什么在Agda中使用可判断性如此困难，而在Coq中它看起来像黄油一样顺利。当我试图证明这个关于字符串的简单定理时，Agda展开了这个混乱的定义，除非你确切地知道你想要做什么，否则几乎不可能使用它。如何通过模式匹配来处理字符串的可判断性，使定义保持得体？ 我正在使用Stump的keep函数，而不是Agda的inspect。 keep : ∀{ℓ}{A : Set ℓ} → (x : A) → Σ A (λ y → x ≡ y)
keep x = ( x , refl )
--first roadblock
eqbStringrefl'
浏览 16提问于2020-04-14得票数 2
回答已采纳
我有一个将自然数映射到其对应的Agda宇宙级别的函数。 level : Nat -> Level
level zero = lzero
level (suc l) = lsuc (level l)
Setn : (l : Nat) -> Set (level (suc l))
Setn l = Set (level l) 我在定义归纳数据类型时以如下方式使用此函数： data U l : Setn l where
...
Lift : {l' : Nat} -> {l' <= l} -> U l' -> U l 在这里，A
浏览 15提问于2020-07-06得票数 4
回答已采纳
1回答
我有一个编程语言的AST的数据类型，我想解释一下，但AST大约有10个不同的构造函数。
data Term : Set where
UnitTerm : Term
VarTerm : Var -> Term
...
SeqTerm : Term -> Term -> Term
我正在尝试编写一个函数，它对这种语言的语法树具有可判定的等价性。从理论上讲，这很简单:没有什么太复杂的，它只是存储在AST中的简单数据。
问题是，编写这样一个函数似乎需要大约100个用例:对于每个构造函数，有10个用例。
eqDecide : (x : Term) -> (y
浏览 0提问于2017-07-18得票数 2
1回答
命题等式的可判性
、、
agda中的两个术语被认为是定义相等的，当它们都具有相同的范式时-我认为-命题相等只是定义相等的数据类型表示-我猜-；那么命题相等不应该是可确定的吗？也就是说，我们可以编写一个类型化的函数看起来合理吗
∀{A : Set} → (x y : A) → Dec(x ≡ y)。
我有点明白，我们不能写这样的函数，因为我们不能对参数进行模式匹配，但我“觉得”这应该是可能的:再说一次，只需简化为标准形式并检查语法一致性。
任何洞察力都会有所帮助！
浏览 1提问于2015-12-16得票数 2
1回答
如何使用Idris构建一个函数，在给定一个字符串的情况下，返回该字符串是十六进制的证明(例如，0x后跟来自0-9和a-f的2*N字符，例如"0x1a7f33b8")？
我尝试过的
首先，我为十六进制字符构造了以下类型：
data IsNib : Char -> Type where
IsNib0 : IsNib '0'
IsNib1 : IsNib '1'
IsNib2 : IsNib '2'
IsNib3 : IsNib '3'
IsNib4 : IsNib '4'
浏览 7提问于2018-01-06得票数 0
1回答
下面是我对Relation.Binary.PropositionalEquality.TrustMe.trustMe的理解:它似乎需要一个任意的x和y，并且：
如果x和y是真正平等的，它就变成refl
如果它们不是，它的行为就像postulate lie : x ≡ y。
现在，在后一种情况下，它可以很容易地使Agda不一致，但这本身并不是一个问题:它只是意味着使用trustMe的任何证明都是向权威机构提出的证明。此外，尽管您可以使用这样的东西来编写coerce : {A B : Set} -> A -> B，但是事实证明，coerce {ℕ} {Bool} 0并没
浏览 2提问于2013-12-16得票数 5
回答已采纳
我有这样的功能：
open import Data.Char
open import Data.Nat
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning
foo : Char → Char → ℕ
foo c1 c2 with c1 == c2
... | true = 123
... | false = 456
我想证明，当我用相同的参数(foo c c)调用它时，它总是产生123
foo
浏览 4提问于2022-06-28得票数 3
回答已采纳
2回答
我想知道Agda中是否有类似于Haskell的deriving Eq条款的东西--那么我下面也有一个相关的问题。
例如，假设我有玩具语言的类型，
data Type : Set where
Nat : Type
Prp : Type
然后通过模式匹配和C-c C-a实现可判定等式，
_≟ₜ_ : Decidable {A = Type} _≡_
Nat ≟ₜ Nat = yes refl
Nat ≟ₜ Prp = no (λ ())
Prp ≟ₜ Nat = no (λ ())
Prp ≟ₜ Prp = yes refl
我很好奇，这是否可以被机械化或自动化，在某种程度上类似于在Ha
浏览 1提问于2016-03-24得票数 7
回答已采纳
1回答
我是Agda新手，我需要帮助来理解Decidable函数和Dec类型。
我正在尝试定义一个一阶逻辑谓词，并且我想用证明来编码某种布尔值。我发现这样做的方法是使用Dec类型。
现在，据我所知，要做到这一点，我必须将所有逻辑运算符重新定义为可判定类型，而不是集合类型。为此，我将其嵌入到了新类型中，这就是我为and运算符所做的：
data _∧_ (A B : Set) : Set where
_&_ : A → B → A ∧ B
Dec∧ : {A B : Set} → A ∧ B → Dec (A ∧ B)
Dec∧ A∧B = yes (A∧B)
这是做这件事的方法，
浏览 6提问于2014-03-13得票数 2
1回答
我想从库中使用与count_occ函数相关的引理(Count_occ_In)。我已经在Coq脚本中导入了库。但是我还是不能使用它。如果我从scipt中的库中复制count_occ & eq_dec，那么它就可以工作。我的问题是，当我已经包含了库模块时，为什么要重新定义函数。请指导我如何仅通过添加库模块来编写引理(不再定义函数)？
浏览 23提问于2021-04-15得票数 1
3回答
Agda和Idris都有效地禁止了Type类型值的模式匹配。看起来Agda总是在第一种情况下匹配，而Idris只是抛出一个错误。
那么，为什么打字是件坏事？它会破坏一致性吗？我还没有找到很多关于这个话题的信息。
浏览 8提问于2014-04-22得票数 50
回答已采纳
1回答
我试图定义一个简单的谓词，以确定公式是否是一个给定形式的子公式，而不是简单的归纳定义的语法。我遇到了一些，大概很简单的问题。
(i)我宁愿使用具有给定类型A的参数化模块。在A具有可判定的相等性的意义下，如何导入A是一个集合的信息？如果不能这样做，有什么解决办法呢？这就是为什么我有Nat的原因。
(ii) t1 ≡ (t2 // t3) (和相似定义的)谓词是否是处理相等子公式的适当方法？如果不这样做，还怎么容易做到这一点呢？我还考虑过为equalFmla编写一个谓词，然后用isSubFormula ⊎ equalFmla创建一个全局子公式谓词，但不确定这是否如此清晰。
(三)当我的图案与第一条
浏览 5提问于2020-10-14得票数 1
回答已采纳
在Agda中，似乎通常有两种改进集合的方法。一种方法是简单地编写一个函数，检查一个属性是否持有，并将其解除。例如：
has_true : List Bool -> Bool
has_true (true ∷ xs) = true
has_true (false ∷ xs) = has_true xs
has_true [] = false
Truthy : List Bool -> Set
Truthy list = T (has_true list)
在这里，Truthy list是一个证明一个布尔列表至少有一个真正的元素。另一种方法是将该属性直接编码为归纳类型：
data
浏览 0提问于2018-09-06得票数 1
回答已采纳
哪种依赖类型的编程语言可以用于实际的应用程序开发？
以下是我认为很重要的几点：
文档
示例程序
标准图书馆
或者至少是一个易于使用的外部函数接口。
使用语言执行真实世界任务的人群。
工具支撑
浏览 0提问于2011-01-08得票数 14
回答已采纳
我想用这个定义来假设集合R成员的某些等式成立：
Definition wiring: Prop
(globalHasVoltage -> (voltageOf voltageIn) = vcc)
/\
(globalHasGround -> (
(voltageOf control) = zero
/\
(voltageOf ground) = zero
浏览 4提问于2022-04-24得票数 0
2回答
我开始深入研究依赖类型编程，并发现Agda和Idris语言最接近Haskell，所以我从那里开始。
我的问题是:它们之间的主要区别是什么？类型系统在这两种语言中的表现形式是否相同？如果能有一个全面的比较和关于好处的讨论，那就太好了。
我已经发现了一些：
Idris有类似于Haskell的类型类，而Agda使用实例argumentsIdris包括一元和应用符号，它们似乎都有某种可重新绑定的语法，尽管不能真正确定它们是否相同。
编辑:这个问题的Reddit页面上有更多的答案：
浏览 75提问于2012-02-28得票数 181
回答已采纳
对于自然数nat这样的简单归纳型，很容易证明两个构造函数(0和后继)给出了所有可能的自然数，
Lemma nat_destruct (n : nat) : n = O \/ exists m : nat, n = S m.
Proof.
destruct n. left. reflexivity. right. exists n. reflexivity.
Qed.
然而，我听说平等证明并不是那么简单。只有一个等式构造函数eq_refl，但是Coq不能证明
eq_destruct : forall (A : Type) (x : A) (prEq : x = x), prEq = eq_r
浏览 0提问于2018-09-12得票数 1
回答已采纳
在立体Agda中，我如何证明两件事是不平等的？(v2.6.1，立体式回购版acabbd9)
具体来说，下面是作为更高归纳类型的整数：
{-# OPTIONS --safe --warning=error --cubical --without-K #-}
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
module Integers where
data False : Set where
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
{
浏览 6提问于2020-04-26得票数 4
回答已采纳
1回答
我是Agda的新手，我试图定义一个类型为prod的常量Z → (Z → ((Z → Set) → Set))：Z → (Z → ((Z → Set) → Set))
现在，我编写了以下Agda代码：
data Prod (X : Set) : ℕ → X where
prod : ℕ → (ℕ → ((ℕ → X) → X))
当我键入它时，agda会生成以下错误消息：
X != Set (_33 X_) of type Set
when checking the definition of Prod
任何帮助都是非常感谢的。
浏览 0提问于2014-02-24得票数 1
回答已采纳
大多数与Agda的交互都是用EMACS完成的，但是有没有办法以编程的方式完成呢？也就是说，是否可以通过命令行或某些API完成所有操作？主要目标是构建一个瘦包装器，以便我们可以从另一种语言(例如：
var Agda = require("agda");
var code = `
data Bool: Set where
true: Bool
false: Bool
not : Bool -> Bool
not true = false
not false = true
val : Bool
浏览 1提问于2018-10-10得票数 3
回答已采纳
1回答
嗨，我想我不太明白如何在Data/Vec.agda中使用Vec.filter。 我知道如何“过滤”(保留)向量中的元素。 filterProof : v.filter (λ e → e ≟ 2) (2 v.∷ v.[]) ≡ (2 vb.∷ vb.[])
filterProof = refl 然而，我不确定如何“过滤”元素。 filterProof : v.filter (λ e → e ? 2) (2 v.∷ v.[]) ≡ vb.[]
filterProof = refl 我不知道?在哪会发生什么。我知道类型必须是Relation.Nullary.Dec，但不确定如何使用Relation
浏览 16提问于2020-11-03得票数 0
回答已采纳
当查看可判定相等类型的结果时(特别是在中)，有一些结果(对于A类型)是需要的
forall x y : A, x = y \/ x <> y
而有些人则要求
forall x y : A, {x = y} + {x <> y}
我的印象是，这是最后一个被称为可决定的平等，但我非常不确定的差别是什么。我知道x = y \/ x <> y在Prop和{x = y} + {x <> y}中是在Set中，我可以证明第一个是从第二个，而不是反过来。据我所知，这是因为不允许我从Prop类型的值构造Set类型的值。
有人能分辨出两者的区别吗？是否有某种
浏览 1提问于2021-10-25得票数 4
回答已采纳
是否有可能定义一个简单的相等语法概念(类似于GHC可能自动派生为Haskell 98类型的Eq实例)，而不显式地证明每个数据构造函数是内射的，或者执行类似的操作，例如定义每个构造函数的回缩和使用cong？
换句话说，是否有可能更直接地利用数据构造函数的内射性，而不是每个构造函数引入一个辅助函数？
下面以自然数为例。
module Eq where
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import R
浏览 3提问于2014-10-10得票数 11
回答已采纳
例如，在Agda中表示STLC可以作为：
data Type : Set where
* : Type
_⇒_ : (S T : Type) → Type
data Context : Set where
ε : Context
_,_ : (Γ : Context) (S : Type) → Context
data _∋_ : Context → Type → Set where
here : ∀ {Γ S} → (Γ , S) ∋ S
there : ∀ {Γ S T} (i : Γ ∋ S) → (Γ , T) ∋ S
data Term : Context → Typ
浏览 0提问于2019-03-01得票数 3
回答已采纳
我有一些代码如下所示：
allLessThan : Ord t => (v1 : Vect n t) -> (v2 : Vect n t) -> Bool
allLessThan v1 v2 = all (\(x,y) => x < y) (zip v1 v2)
unravelIndexUnsafe : (order : ArrayOrder) ->
(shape : ArrayShape (S n)) ->
(position : Vect (S n) Nat) -
浏览 4提问于2021-06-27得票数 1
回答已采纳
1回答
为什么自定义单位类型不允许我们证明这个基本的左单位定律？我看到我的实现和标准库之间的唯一区别是使用了Record和Data归纳类型。我不明白为什么Data不允许我证明这个基本的左恒等引理，这应该是绝对正确的。这与Record的自动eta继承有关吗?如果是，为什么会这样?有没有可能在没有内置(例如Record)单元类型的情况下证明这一点?一般来说，这是Data的限制，还是可以在agda模数记录中做所有的事情？ data _≡_ {A : Set} : A → A → Set where
refl : (a : A) → a ≡ a
--from builtin
lunitm : (f :
浏览 11提问于2020-07-17得票数 1
回答已采纳
如果需要的话，必须在Coq中以公理方式添加UIP (以及类似于公理K的等价物)：
uip : ∀ A (x y: A) (p q: x = y), p = q
这是令人惊讶的，因为从等式的定义来看，这是显而易见的，它只有一个构造函数。(当然，这取决于对Coq中归纳定义包含其类型的所有元素的解释)。
当你试图证明UIP时，你会被困在反身子大小写上：
uip_refl : ∀ A (x: A) (h: x = x), h = eq_refl x
我们可能希望下面这个术语是一个恰当的证明术语：
fun A (x: A) (h: x = x) =>
match h as h0 in (_ =
浏览 5提问于2021-12-22得票数 3
回答已采纳
我正在运行预置的Windows版本2.4.2.2。在Emacs/agda 2中，包括Dirs，我已经识别了c:/Agda2 0.13/src和下面一个级别的文件夹。在加载一个只包含这两行的模块时，我会收到一条错误消息。
module test1 where
open import Integer
错误信息：
C:\agda-stdlib-0.13\src\Data\Empty.agda:13,5-5
C:\agda-stdlib-0.13\src\Data\Empty.agda:13,5: Parse error
HASKELL<ERROR> data AgdaEmpty #-}
浏览 1提问于2017-07-15得票数 1
回答已采纳
使用下面的Agda代码，我在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 module B. Previous definition of datatype
module B at /home/cactus/prog/agda/modules.agda:4,8-9
when scope che
浏览 0提问于2013-04-23得票数 3
回答已采纳
为什么模式匹配有时在Agda中是“必不可少的”？
我要把这个从里拿出来。
当不进行模式匹配时，Agda给出的不允许refl进入洞：
η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× x = ?
它报告了这个目标和假设：
Goal: ⟨ proj₁ x , proj₂ x ⟩ ≡ x
————————————————————————————————————————————————————————————
x : A × B
但是，如果我告诉它案例拆分(ctrl-c ctrl-c x Ret) )，Agda就能搞清楚到底
浏览 1提问于2019-09-06得票数 2
回答已采纳
我在上找不到这方面的信息，在“agda中的验证编程”.What上也找不到这方面的信息，这是否意味着？我从哪里可以知道更多像这样的错误？
完全错误是.cter !=< cter of type Set
代码有点像missy，所以如果需要的话，我会稍后发布它，这是关于实现模拟退火算法的。
浏览 2提问于2018-02-27得票数 2
回答已采纳
下面的Agda函数应该查找一个列表，循环索引溢出：
module Test where
open import Prelude.Nat
open import Prelude.List
roundIndex : {A : Set} -> Nat -> A -> List A -> A
roundIndex n x xs = go n xs where
go : {A : Set} -> Nat -> List A -> A
go (suc n) (x ∷ xs) = go n xs
go (suc n) [] = go n
浏览 0提问于2018-03-23得票数 2
回答已采纳
我刚刚为我在python中的一个项目编写了一个测试脚本，并且我了解到，检查两个对象的值是否等价并不像foo == bar那么简单。例如，我有一个对象dashboard，它的属性是熊猫数据，所以我将它的__eq__方法定义为：
def __eq__(self, other):
vals = [self.__dict__[k] == other.__dict__[k] for k in self.__dict__.keys()]
vals = [v if isinstance(v, bool) else all(v) for v in vals]
return all(va
浏览 4提问于2017-09-16得票数 1
回答已采纳
我还需要一个引理来证明inj₁ x ≡ inj₂ y是荒谬的，它是Agda中关于不相交并型(⊎)的一个较大定理的一部分。
这个结果将直接来自于⊎**，的两个构造函数，即** inj₁ 和 inj₂**，不相交。**在Agda中是这样的吗？我该怎么证明呢？
以下是完整的引理：
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Sum
lemma : ∀ {a b} {A : Set a} {B : Set b} {x : A} {y : B} → ¬
浏览 1提问于2015-01-31得票数 4
回答已采纳
我可能不会这么做，因为Agda，特别是，Agda标准库对我来说还是很新的。我正在尝试实现一些二进制搜索树的概念。
我对二叉树有一个简单的定义。
data BTree (A : Set) : ℕ → Set where
Leaf : A → BTree A 1
Node : ∀ {n m} → A → BTree A n → BTree A m → BTree A (1 + n + m)
以及从二叉树中提取最大值和最小值的两个函数bt-⊔ : ∀ {n : ℕ} → BTree ℕ n → ℕ和bt-⊓ : ∀ {n : ℕ} → BTree ℕ n → ℕ。
我现在试图定义一种数据类型
浏览 3提问于2016-04-13得票数 3
回答已采纳
有没有办法比较两个函数的相等性？例如，(λx.2*x) == (λx.x+x)应该返回true，因为它们显然是等价的。
浏览 1提问于2013-06-11得票数 75
回答已采纳
1回答
我试图证明一个矛盾，但我遇到了一个问题，试图向Agda证明由<>-wt-inv返回的sigma域类型与前面的证明中所看到的相同。我希望uniq型的证据能帮到我，但我不能把它们合在一起。
我希望下面代码中的评论能够给出足够的上下文。
-- given a type for (f ⟨⟩), we can derive that f is a function type
-- and we can prove that the context yields σ
⟨⟩-wt-inv : ∀ {n m f τ} {K : Ktx n m} → K ⊢ (f ⟨⟩) ∶ τ →
浏览 1提问于2015-04-07得票数 3
回答已采纳
1回答
我一直在Agda的编程语言基础上工作，目前我正在学习“决策:布尔人和决策过程”。看起来，至少在给出的详细示例中，判断某物是否为真的函数在结构上类似于一个证明对象，它演示了为什么它是真的。特别是证明类型
data _≤_ : ℕ → ℕ → Set where
z≤n : ∀ {n : ℕ} → zero ≤ n
s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n
具有与决策函数相同的结构。
_≤ᵇ_ : ℕ → ℕ → Bool
zero ≤ᵇ n = true
suc m ≤ᵇ zero = false
suc m ≤ᵇ suc n
浏览 6提问于2022-10-31得票数 2
回答已采纳
我对类型理论和依赖类型编程非常陌生，最近正在尝试Agda的各种功能。下面是我编写的记录类型C的一个非常简单的示例，它包含多个组件记录和一些我们可以用来证明东西的约束条件。
open import Relation.Binary.PropositionalEquality
module Sample (α : Set) where
record A (type : α) : Set where
record B : Set where
field
type : α
record C : Set where
field
b₁ : B
浏览 3提问于2019-04-12得票数 3
在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 ≡ λ ()不应该是某种形式的eta法吗？
浏览 4提问于2020-03-26得票数 2
回答已采纳
2回答
我已经开始玩立体Agda了。我做的最后一件事是以一种类似于古典数学中所做的方式来构建整数的类型(假设自然数的类型已经定义)(参见)。这是
data dInt : Set where
_⊝_ : ℕ → ℕ → dInt
canc : ∀ a b c d → a + d ≡ b + c → a ⊝ b ≡ c ⊝ d
trunc : isSet (dInt)
做完之后，我想定义加法。
_++_ : dInt → dInt → dInt
(x ⊝ z) ++ (u ⊝ v) = (x + u) ⊝ (z + v)
(x ⊝ z) ++ canc a b c d u i
浏览 6提问于2021-11-13得票数 2
回答已采纳
1回答
我已经使用Agda 9个月了。这是我第一次发现自己想要“运行”(作为顶级可执行文件)--一个打印字符串的Agda程序。叫我老派。
我可以编写一个计算字符串的程序，并获得Agda来显示交互模式(或Emacs)中字符串的值。但是字符串很长，并嵌入了新行。我想把它打印出来。
相比之下，在GHCi中我可以这样做：
Prelude> putStrLn "hello, world!"
hello, world!
但在Agda的互动模式中，我得到了这样的信息：
Main> putStrLn "hello, world!"
.IO.♯-15
('h'
浏览 1提问于2014-09-25得票数 6
回答已采纳
1回答
下面证明了两个函数的等价性： η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f
η-→ f = refl 为什么它不需要可扩展性？Agda如何知道≡左边的函数简化为f
浏览 19提问于2019-09-07得票数 3
回答已采纳
考虑以下目标： Goal forall (x y: I = I), x = y.
Proof.
Abort.
Goal forall (x y: tt = tt), x = y.
Proof.
Abort. I和tt都是单例类型的成员。前者住在Prop，后者住在Set。这些都是非常简单的类型，所以我不期望它们在任何设置中都支持丰富的相等类型。在不借助身份证明公理的唯一性的情况下，这些目标在Coq中是可以证明的吗？
浏览 20提问于2020-06-27得票数 1
回答已采纳
1回答
在依赖类型的编程中，定义
data Vec :: Type -> Nat -> Type where
Nil :: Vec a 'Z
Cons :: a -> Vec a n -> Vec a ('S n)
然而，在Haskell，Functor、Applicative、Foldable、Traversable、Eq1、Ord1等，类似乎是一个很好的理由，可以把争论转到Vec :: Nat -> Type -> Type上。
常规会议有什么重要的原因吗？还是仅仅是人们在语言中使用的东西，而不是基本上基于类型类？
浏览 1提问于2016-09-28得票数 4
回答已采纳
有基于高阶逻辑(HOL)的编程语言和定理证明器。例如、、。例如，12 is既是一种编程语言，也是一种定理证明器，而Isabelle主要是一种定理证明器，但是对于Isabelle来说，代码提取是可用的。
我正在寻找一个基于haskell的HOL编程语言。原因是我非常喜欢lambda，但它并不是一种实用的编程语言。Lambda缺乏一个标准库，与外部库的接口看起来并不简单。问题是，如果您需要一些功能，比如为文本文件编写解析器，那么就不能与haskell的许多可用的现有库进行接口，而且也没有标准库，因此您可以从头开始。
今天，我遇到了作为硕士论文实现的编程语言。来自github页面：
Caledon
浏览 3提问于2015-01-09得票数 7
回答已采纳
1回答
在Coq标准库中，自然数(lt_dec)和整数(Z_lt_dec)的“小于”关系是可确定的。然而，当我搜索(Search ({ _ _ _ } + {~ _ _ _ }))时，我找不到Q_le_dec或Qle_dec来寻找有理数，只能找到Qeq_dec来寻找可判定的相等。
这是不是因为“小于”关系对于Coq中的逻辑来说是不可确定的？或者它是可确定的，但决策过程只是没有在标准库中实现？
浏览 3提问于2021-11-03得票数 3
我试图公理化一个证明无关的分离命题与类型消除在Agda中使用。然而，当我试图为计算规则定义重写规则时，我会得到一个关于某个变量未被绑定的错误。例如，以一个最小的例子为例，以下代码没有编译：
{-# OPTIONS --rewriting --prop #-}
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
module Disjunction where
private variable
α β : Prop
A : Set
postulate
_∨_ : (α : Pr
浏览 8提问于2022-09-05得票数 0
回答已采纳
1回答
Agda中的“严格正”
、、、、
我试图根据我用Haskell编写的程序将一些表示语义编码到Agda中。
data Value = FunVal (Value -> Value)
| PriVal Int
| ConVal Id [Value]
| Error String
在Agda中，直接翻译是；
data Value : Set where
FunVal : (Value -> Value) -> Value
PriVal : ℕ -> Value
ConVal : String -> List Va
浏览 1提问于2010-04-06得票数 28
回答已采纳
var Answer = '2a + 5b' // downloaded from database
var input = '5*b+ 2*a' // user input after calculating some algebraic expression.
if (Answer == input){
// tell student he solved the math problem correctly.
}
我想要一个函数，这样上面的if语句就会返回true。我的问题是，我的答案和用户输入是一个字符串，当比较时，它们是不相等的。然而，用户
浏览 0提问于2020-03-27得票数 0
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
实时音视频活动推荐
腾讯云开发者
