问题标签 [fstar]

FStar 需要大约 2 分钟来证明这个引理，更糟糕的是，只要它存在，Emacs 就会变得难以忍受。其他显然更复杂的引理不会导致此问题。

是否有与此问题相关的 Emacs/FStar 选项？

我刚开始学习FStar。我想表达一个事实，即每一个自然数都存在一个更大的数。

它失败了，我想知道为什么。谢谢你。

我能简要解释一下为什么这个证明工作会失败吗？在我的研究中，我试图识别生成的整数列表中的简单模式。下面的生成器生成一个交替的 0 和 1 列表。我想证明偶数索引处的项目为 0。

FStar 返回“无法证明后置条件”。我将不胜感激有关该方法的任何帮助。

我想了解这个简单的练习有什么问题。

FStar 返回“（错误）未知断言失败”。

我正在尝试从 FStar 教程中了解矢量类型：

构造向量 - 类似于构造普通列表 -Cons nat 3 Nil失败，whileCons nat 3被接受。Cons有人可以通过阅读需要尾部参数来向我解释我错在哪里吗？此外，如何创建具有实际元素的向量 - 还是“空向量”类型？

I'm using F* 0.9.6.0 and I can't get this simple program to pass subtyping checks:

I would expect english to pass but invalid to fail. Everything I've tried either leads to both of them being rejected, or both being accepted. What am I doing wrong? I'd just like to accept strings of certain lengths for this type.

以下简单函数被接受为终止函数似乎是不正确的：

令人惊讶的是，该函数确实在评估它时终止，例如，通过fnc 0 0 1和返回false。我错过了什么？

我想了解为什么不接受此功能作为终止功能：

FStar 拒绝它并发送以下消息：

（错误）无法证明此递归调用的终止：求解器找到了一个（部分）反例......

这里的绑定问题可能与我在FStar 函数奇怪行为下的相关问题中的绑定问题不同

FStar 可以举出反例吗？

函数式程序效率低下的一个典型案例是reverse从规范编写的函数

使用关联性，可以得出一个有效的反向

但是，问题首先来自哪里？

• 我们指示特定的订单++
• 由我们的语言定义的组合定义了我们的组合的顺序++
• 我们的语言不知道法律，源于代码本身，也不知道效率的概念。

我们真正想做的是：

• 指定一个（函数）关系++，由它的所有定律正确商化
• 为它使用关系组合，它隐藏了将使用哪个特定的括号
• 在使用站点，选择一个最适合我们的访问模式和目标的括号（在 的情况下reverse，这意味着移动所有括号以匹配结果列表的构造方式）

是否有任何语言可以产生一些规律，并根据一些指标寻找最好的重写？

我正在使用 emacs fstar 模式浏览​​ fstar 教程。有没有办法评估表达式或其类型？

我正在寻找的是相当于精益的#check 或#eval。