在emacs中加载文件时(通过find-file),emacs将文件加载到具有适当模式的缓冲区中,调用适当的处理程序等.有时,为了调试,我希望能够将文件直接加载到基本文件中模式,不触发任何其他内容.这样做最简单的方法是什么？
我正在尝试Num在OCaml中使用该模块(bignums和big fractions).有些东西似乎有效,而有些东西似乎没有,而且我无法生成一个完整的例子.例如:
# Num.Int(234);;
- : Num.num = Num.Int 234
# Num.mult_num;;
Characters -1--1:
Num.mult_num;;
Error: Reference to undefined global `Num'
我可以问一个两个bignums相乘的简单例子吗？
参考Num是在这里.
此问题与在Emacs中的Proof General中配置Coq模式有关.
我正在尝试让Emacs使用相应的Unicode字形自动替换Coq中的关键字和符号.我设法定义fun为希腊小写lambdaλ,forall作为通用量词符号∀等.我没有问题定义单词的符号.
问题是,当我尝试定义操作符=>,->,<->等他们的Unicode符号⇒→↔,他们不是在勒柯克相应的Unicode字形所取代.但是,*scratch*当我测试它们时,它们会在缓冲区中被替换.我使用相同的机制将Unicode glyps与Coq表示法匹配:
(defun define-glyph (string char-info)
(font-lock-add-keywords
nil
`((,(format "\\<%s\\>" string)
(0 (progn
(compose-region
(match-beginning 0) (match-end 0)
,(apply #'make-char char-info))
nil))))
))
我怀疑问题是Coq模式将某些标点符号标记为特殊标记,因此Emacs忽略了我的代码以用Unicode字形替换它们,但我不确定.有人可以帮我解释一下吗？
我试图在Coq中定义Ackermann-Peters函数,我收到一条我不明白的错误消息.正如你所看到的,我把a, bAckermann 的论据打包成一对ab; 我提供了一个定义参数的排序函数的排序.然后我使用Function表单来定义Ackermann本身,为它提供ab参数的排序函数.
Require Import Recdef.
Definition ack_ordering (ab1 ab2 : nat * nat) :=
match (ab1, ab2) with
|((a1, b1), (a2, b2)) =>
(a1 > a2) \/ ((a1 = a2) /\ (b1 > b2))
end.
Function ack (ab : nat * nat) {wf ack_ordering} : nat :=
match ab with
| (0, b) => b + 1
| (a, 0) => ack (a-1, 1)
| (a, b) => ack (a-1, …有人可以给我一个关于Coq存在实例化和存在概括的简单例子吗？当我想要证明exists x, P,在P某些地方Prop使用时x,我经常想要命名x(作为x0或某些),并操纵P.这可能是Coq中的一个吗？
我试图证明一个关于道具的替代定理,而且我失败了.可以在coq中证明以下定理,如果不是,为什么不.
Theorem prop_subst:
forall (f : Prop -> Prop) (P Q : Prop),
(P <-> Q) -> ((f P) <-> (f Q)).
关键是逻辑上的证据是归纳的.就我所见,Prop没有归纳定义.如何在Coq中证明这样的定理？
Coq的文档带有一般警告,不依赖于内置命名机制,而是选择自己的名称,以免命名机制中的更改过去证明无效.
在考虑表单的表达式时remember Expr as v,我们将变量v设置为表达式Expr.但是假设的名称是自动选择的,就像这样Heqv,我们有:
Heqv: v = Expr
我怎样才能选择自己的名字而不是Heqv？我总是可以使用rename命令将它重命名为我喜欢的任何内容,但这并不能保证我的证明不依赖于Coq中内置命名机制的假设未来变化.
我需要参考编号列表中的项目编号.例如:
1. Something
2. See item (1)
3. Something else
Orgmode让我创建超链接,但这些在打印文档中没用,所以我需要参考项目的实际编号.我并不挑剔它的呈现方式(1),<1>,1等等都可以满足我的需求.
字符*和?用作路径名中的通配符。如何引用具有?实际字符之一的文件名？例如：
[18]> (wild-pathname-p #p"foo")
NIL
[19]> (wild-pathname-p #p"foo?")
T
那么引用文件名“foo？” 不能这样做。我试图用?反斜杠转义，但这没有用。\u3f我尝试使用or转为 unicode \u003f，但这不起作用。
如何引用名称中包含通配符的文件：如何探测、打开它等？