问题标签 [agda]

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

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

应该返回BoolProp false

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

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

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

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

这些已经导入：

我们需要实现这个扩大 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？

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

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

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

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

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

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

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

我正在尝试解析 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

首先是一些无聊的导入：

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

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

酒吧的目标是

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

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

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

但是，以下具有类型Set：

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