在Coq中找到类似++的定义和符号 [英] Find the definition and notations like ++ in Coq

问题描述

我们如何获得这些符号的定义/类型，例如 + 或 ++ 列表的？

How can we get the definition/type for those notations like "+", or "++" of List?

我尝试过：搜索++ ，搜索 ++ ，搜索（++），
SearchAbout ... 和
检查++ ，检查 ++ ，检查（++）。

I have tried : Search ++, Search "++", Search (++), SearchAbout ... and Check ++, Check "++", Check(++).

但是它们都不起作用...

None of them work however...

SearchAbout ++ 确实显示了一些信息，但没有显示 ++ 的定义。

SearchAbout "++" does show some info, but not the definition of "++".

推荐答案

执行：

Locate "++".

要查找符号。

然后您可以打印 / 检查所表示的实际术语。

Then you can Print/Check the actual term being denoted.

这篇关于在Coq中找到类似++的定义和符号的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！