在 Coq 中查找 ++ 等定义和符号

2024-03-29

我们如何获得这些符号的定义/类型,例如"+", or "++" of List?

我努力了 :Search ++, Search "++", Search (++), SearchAbout ... and Check ++, Check "++", Check(++).

然而它们都不起作用......

SearchAbout "++"确实显示了一些信息,但没有显示定义"++".


Do:

Locate "++".

查找符号。

然后你可以Print/Check所表示的实际术语。

本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)

在 Coq 中查找 ++ 等定义和符号 的相关文章

随机推荐