Coq 导入电源问题-6ren

Coq 导入电源问题

转载作者：行者123 更新时间：2023-12-04 10:03:58

28

4

看来我无法正确获取 Coq 导入系统。

我找到了pow_succ_r在 Coq.Arith.PeanoNat .

所以我导入了它，希望它可以使用

Require Import Coq.Arith.PeanoNat.
Print pow_succ_r.

我收到以下错误:

pow_succ_r not a defined object.

最佳答案

注意行 Module Nat文档顶部附近。这意味着后面的声明在Nat里面。模块。因此，您可以将符号访问为 Nat.pow_succ_r .

一般来说，如果您要查找符号，请使用 Locate命令:

Locate pow_succ_r.
(*
Constant
  Coq.Arith.PeanoNat.Nat.pow_succ_r
  (shorter name to refer to it in current context is Nat.pow_succ_r)
*)

关于Coq 导入电源问题，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/61685279/

28

4

0

文章推荐： r - 在 Shiny 中抑制数据表中的排序

文章推荐： r - 在lubridate中增加15个工作日

文章推荐： python - 使用经过训练的 TensorFlow 模型预测单个 PNG 图像

问题
关闭。这个问题是off-topic .它目前不接受答案。想要改进这个问题？ Update the question所以它是on-topic用于堆栈溢出。关闭 12 年前。 Improve thi
问题
我有一个动态网格，其中的数据功能需要正常工作，这样我才能逐步复制网格中的数据。假设在第 5 行中，我输入 10，则从第 6 行开始的后续行应从 11 开始读取，依此类推。如果我转到空白的第一行并输入
问题
我有一个关于我的按钮消失的问题我已经把一个图像作为我的按钮用这个函数动画 function example_animate(px) { $('#cont
php - 将现有帐户链接到 Facebook - 问题/问题
我有一个具有 Facebook 连接和经典用户名/密码登录的网站。目前，如果用户单击 facebook_connect 按钮，系统即可运行。但是，我想将现有帐户链接到 facebook，因为用户可以选
iOS map View 问题/问题
我有一个正在为 iOS 开发的应用程序，该应用程序执行以下操作加载和设置注释并启动核心定位和缩放到位置。 map 上有很多注释，从数据加载不会花很长时间，但将它们实际渲染到 map 上需要一段时间。
ruby-on-rails - Heroku，问题/问题
我被推荐使用 Heroku for Ruby on Rails 托管，到目前为止，我认为我真的会喜欢它。只是想知道是否有人可以帮助我找出问题所在。我按照那里的说明在该网站上创建应用程序，创建并提交
Android WebView setCertificate 问题 SSL 问题
我看过很多关于 SSL 错误的帖子和信息，我自己也偶然发现了一个。我正在尝试使用 GlobalSign CA BE 证书通过 Android WebView 访问网页，但出现了不可信错误。对于大多
c++ - Glew 问题， Unresolved external 问题
我想开始使用 OpenGL 3+ 和 4，但我在使用 Glew 时遇到了问题。我试图将 glew32.lib 包含在附加依赖项中，并且我已将库和 .dll 移动到主文件夹中，因此不应该有任何路径问题。
问题？
我已经盯着这两个下载页面的源代码看了一段时间，但我似乎找不到问题。我有两个下载页面，一个 javascript 可以工作，一个没有。工作:http://justupload.it/v/lfd7不是
jquery - 初级 jQuery 问题(FF/IE 问题)
我一直在使用 jQuery，只是尝试在单击链接时替换文本字段以及隐藏/显示内容项。它似乎在 IE 中工作得很好，但我似乎无法让它在 FF 中工作。我的 jQuery: $(function() {
Android ndk 问题 socket 和 std 问题
我正在尝试为 NDK 编译套接字库，但出现以下两个错误: error: 'close' was not declared in this scope 和 error: 'min' is not a m
java - Selenium 问题 : Select. deselectAll() 导致 iframe 问题
我正在使用 Selenium 浏览器自动化框架测试网站。在测试过程中，我切换到特定的框架，我们将其称为“frame_1”。后来，我在 Select 类中使用了 deselectAll() 方法。不久之
连接到 Heroku PostgreSQL 的 Python 问题 - SSL 问题
我正在尝试通过 Python 创建到 Heroku PostgreSQL 数据库的连接。我将 Windows10 与 Python 3.6.8 和 PostgreSQL 9.6 一起使用。我从“ht
python - 在 Pandas 中创建新列的 np.where() 问题(可能是 NaN 问题？)
我有一个包含 2 列的数据框，我想根据两列之间的比较创建第三列。所以逻辑是:第 1 列 val = 3，第 2 列 val = 4，因此新列值什么都没有第 1 列 val = 3，第 2 列 va
css - 如何调试 iphone 5 中的 css 问题(ui 问题)？
我想知道如何调试 iphone 5 中的 css 问题。我尝试使用 firelite 插件。但是从纵向旋转到横向时，火石占据了整个屏幕。有没有其他方法可以调试 iphone 5 中的 css 问题
CSS 问题，input[id]+label，:hover, 和 :checked 问题
所以我有点难以理解为什么这不起作用。我正在尝试替换我正在处理的示例站点上的类别复选框。我试图让它做以下事情:未选中时以一种方式出现，悬停时以另一种方式出现(选中或未选中)选中时以第三种方式出现(而不是
javascript - 1 javascript/css 问题 2 perl cgi 问题
Javascript CSS 问题: 我正在使用一个文本框来写入一个 div。我使用以下 javascript 获取文本框来执行此操作: function process_input(){
algorithm - NP 中的语言(问题)和 P 中的语言(问题)之间的多项式时间减少
你好，我很难理解 P、NP 和多项式时间缩减的主题。我试过在网上搜索它并问过我的一些 friend ，但我没有得到任何好的答案。我想问一个关于这个话题的一般性问题: 设 A,B 为 P 中的语言(或
python-3.x - 该算法(解决 leetcode 问题 650)(问题 2)的时间复杂度是多少？
你好，我一直在研究 https://leetcode.com/problems/2-keys-keyboard/并想到了这个动态规划问题。您从空白页上的“A”开始，完成后得到一个数字 n，页面上应该
ios - Xcode Server Bot 问题 : warning. 生成服务错误。问题:路径 'some/path' 的存档格式不正确
我正在使用 Cocoapods 和 KIF 在 Xcode 服务器上运行持续集成。我已经成功地为一个项目设置了它来报告每次提交。我现在正在使用第二个项目并收到错误: Bot Issue: warnin

首页

博学

6Ren·AI

商城

Coq 导入电源问题