问题标签 [agda]

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

0 投票
2 回答
510 浏览

haskell - Agda,布尔命题

前言注意这是一个作业。已经针对第一个问题提出了一个问题。所以我们有数据类型:

现在我们被要求写这个命题

应该返回BoolProp false

我只是对如何做到这一点感到困惑。Ptrue但是返回BoolProp true数据类型por采用两个Bool's not BoolProp'。可能是数据类型错误。任何抬头都会很棒

我应该补充一点,eval 代码是 haskell 代码的一个片段

注意:对其进行了编辑以不放弃所有内容

0 投票
1 回答
1071 浏览

agda - Agda 和二叉搜索树

请注意,这是一个作业,所以最好不要发布完整的解决方案,相反,我只是卡住了,需要一些关于我接下来应该看什么的提示。

这些已经导入:

我们需要实现这个扩大 BST 范围的函数:

到目前为止我有这个:

现在这显然不起作用,因为新边界不必严格小于/大于最小值/最大值。给出了一个提示:It is not strictly necessary, but you may find it helpful to implement an auxiliary function that widens the range of a strictly smaller than relation of the form min < max.这就是我在这里所做的,显然我需要改变一些事情,但我认为基本的想法就在那里。

这就是我所处的位置,我只是真的不知道从这里去哪里,我已经做了尽可能多的研究,但是没有很多关于使用 Agda 的阅读材料。我是否可能需要使用 ≤-refl 或 ≤-trans?

0 投票
1 回答
229 浏览

equality - Turning a <= b to suc a <= suc b

0 投票
0 回答
2066 浏览

agda - 是否有在生产中运行的示例 Agda 代码?

Agda 是一种很好的编程语言,可以探索依赖类型,玩转直觉类型理论,并试验这些东西的实现。但是已经有用 Agda 编写的“真实”程序的例子了吗?甚至可能是展示其功能的示例(类似于 xmonad 经常被称为“真实”Haskell 程序的示例)?

0 投票
2 回答
4913 浏览

haskell - 直觉型理论的组合逻辑等价物是什么?

我最近完成了一门以 Haskell 和 Agda(一种依赖类型的函数式编程语言)为特色的大学课程,并且想知道是否可以用组合逻辑替换其中的 lambda 演算。使用 Haskell 似乎可以使用 S 和 K 组合器,从而使其无点。我想知道 Agda 的等价物是什么。即,可以在不使用任何变量的情况下制作一种与 Agda 等效的依赖类型函数式编程语言吗?

此外,是否有可能以某种方式用组合器代替量化?我不知道这是否是巧合,但通用量化例如使类型签名看起来像一个 lambda 表达式。有没有办法从类型签名中删除通用量化而不改变其含义?例如在:

不使用 forall 可以表达同样的事情吗?

0 投票
3 回答
1003 浏览

agda - Agda:用数字解析字符串

0 投票
1 回答
630 浏览

haskell - Agda:我的代码没有类型检查(如何正确获取隐式参数?)

"checkSimple" 获取 u,Universe U 的一个元素,并检查 (nat 1) 是否可以转换为给定 u 的 agda 类型。返回转换的结果。

现在我尝试编写一个控制台程序并从命令行获取“someU”。

因此,我将“checkSimple”的类型更改为包含一个 (u: Maybe U) 作为参数(可能是因为来自控制台的输入可能是“无”)。但是我无法获取代码进行类型检查。

0 投票
3 回答
1010 浏览

parsing - Agda:解析嵌套列表

我正在尝试解析 Agda 中的嵌套列表。我在谷歌上搜索,我发现最接近的是 Haskell 中的解析,但通常使用像“parsec”这样的库,这些库在 Agda 中不可用。

所以我想"((1,2,3),(4,5,6))"(List (List Nat)).

并且应该支持进一步的嵌套列表(直到深度 5),例如,深度 3 将是(List (List (List Nat))).

我的代码很长很麻烦,它只适用于嵌套列表,(List (List Nat))但不适用于进一步的嵌套列表。我自己没有取得任何进展。

如果有帮助,我想重用我的一个旧帖子splitBy第一个答案

编辑1 **

康纳在 ICFP 的演讲是在线的——标题是“Agda-curious?”。
这是两天前的事。看看这个!!
.
观看视频:
http ://www.youtube.com/watch?v=XGyJ519RY6Y

--
EDIT2:
我发现一个链接似乎几乎是我解析所需的代码。
提供了一个tokenize功能:
https ://github.com/fkettelhoit/agda-prelude/blob/master/Examples/PrefixCalculator.agda

--
EDIT3:
我终于找到了一个应该足够快的简单组合库。库中没有包含示例,因此我仍然需要查看如何解决问题。
链接在这里:

https://github.com/crypto-agda/agda-nplib/blob/master/lib/Text/Parser.agda

有更多来自 Nicolas Pouillard 的在线代码:
https ://github.com/crypto-agda

0 投票
1 回答
1738 浏览

agda - 在 agda 中包含 with/rewrite 子句的类型,或者,如何使用 rewrite 而不是 subst?

首先是一些无聊的导入:

现在假设我有一个类型,例如由 naturals 索引。

我想证明在这种类型上运行的函数的一些等式Foo。因为 agda 不是很聪明,所以这些将是异构的平等。一个简单的例子是

酒吧的目标是

这些|目标在做什么?我什至如何开始构建这种类型的术语?

在这种情况下,我可以通过手动进行替换来解决这个问题subst,但是对于较大的类型和方程式来说,这变得非常丑陋和乏味。

0 投票
2 回答
1085 浏览

types - 为什么 (Set -> Set) 不能有 Set 类型?

在 Agda 中, a 的类型以如下方式forall确定:Set1Set1SetASet

但是,以下具有类型Set

我知道如果Set有 type Set,会有矛盾,但我看不出,如果上述三个术语中的任何一个有 type Set,我们就会有矛盾。这些可以用来证明False吗?它们可以用来证明Set : Set吗?