文件名称：coq-tricks:您希望Coq手册告诉您的技巧
文件大小：33KB
文件格式：ZIP
更新时间：2024-05-19 03:36:12
coq Coq
考克的技巧 Coq中的一些技巧，窍门和功能很难发现。 如果您有技巧，可以随时提交问题或请求请求！ 左旋 pattern策略将一个表达式概括为一个变量。 例如， pattern y将P xyz的目标转换为(fun y => P xyz) y 。 使用此方法的一种特别有用的方法是对eval pattern y in constr:(P xyz)进行模式匹配以仅提取函数。 lazymatch就像是match但是不会在match操作内部失败时回溯。 如果您不使用失败进行回溯（通常是这种情况），那么lazymatch会获得更好的错误消息，因为操作内的错误将成为整体错误消息，而不是无关紧要的“ no match”错误消息。 （ match的语义意味着Coq显然不能做得更好-它无法区分操作中的错误和故意使用故障来防止模式匹配。） deex （请参阅 ）是一种有用的策略，用于从exists假设中提
【文件预览】：
coq-tricks-master
----.github()
--------workflows()
----src()
--------Check.v(338B)
--------Instantiate.v(449B)
--------LtacGallinaApplication.v(785B)
--------NoInit.v(369B)
--------ArityDefinition.v(111B)
--------Bidirectional.v(460B)
--------UnshelveInstantiate.v(415B)
--------DivMod.v(835B)
--------DefEquality.v(644B)
--------Modules.v(2KB)
--------CheckEnv.v(1KB)
--------HintLocality.v(1KB)
--------Search.v(2KB)
--------Deex.v(361B)
--------NotationModule.v(918B)
--------Sections.v(1KB)
--------Function.v(4KB)
--------RelationInstances.v(2KB)
--------Macros.v(277B)
--------IntroPatterns.v(768B)
--------Constructors.v(2KB)
--------Learn.v(1KB)
--------SmallInversions.v(653B)
--------Coercions.v(860B)
--------Context.v(776B)
--------InstanceGeneralization.v(603B)
--------RecordFunction.v(272B)
--------Sleep.v(143B)
--------RewNotation.v(316B)
--------TypeParametersAndIndices.v(4KB)
----.gitignore(47B)
----_CoqProject(9B)
----Makefile(223B)
----README.md(26KB)