小编Nec*_*cto的帖子

我对emacs自动完成模式非常兴奋.但是我的代码库很大,有时候,当我输入时,它会尝试ssuggest完成,它搜索所有可能的单词,然后挂起.这很烦人.

有没有办法在后台并行进程中运行搜索,因此emacs仍然会响应用户操作.并且只有当查询结束时该点位于该位置时,建议自动完成？

类似地,键盘输入是主要过程,并且永远不会被延迟,并且自动完成作为机器资源上的残差.

如何在emacs中使后向正则表达式搜索变得贪婪？

例如,我有abc 163439 abc我的缓冲区,我运行 M-x search-backward-regexp 以下正则表达式:163439\|3.这个正则表达式总是会在缓冲区中找到"3",但整个长整数都会更新.因为,当它开始搜索时,它首先会遇到'3'.在第二次尝试中,它将从数字内部的"3"的位置开始,并且将省略它.

如何找到最长和最接近的匹配？

所以我的意思是,当它遇到'3'时,我希望它检查匹配的部分是否不是更大匹配的一部分.

我们如何证明以下内容？：

Lemma forfun: forall (A B : nat->nat), (forall x:nat, A x = B x) ->
                                       (fun x => A x) = (fun x => B x).
Proof.

我需要将顶部被杀死的字符串替换为另一个.我可以(猛拉)它然后(杀死区域......),但在那之后,会有两个字符串:旧字符串和新字符串.如何从杀戮戒指中完全删除旧条目？

我想在一些假设存在的情况下应用规则,而另一个假设不存在.我该如何检查这种情况？

例如:

Variable X Y : Prop.
Axiom A: X -> Y.
Axiom B: X -> Z.

Ltac more_detail :=
    match goal with
     |[H1:X,<not H2:Y>|-_]  =>
      let H' := fresh "DET" in assert Y as H'
                                   by (apply A;assumption)
     |[H1:X,<not H2:Z>|-_]  =>
      let H' := fresh "DET" in assert Z as H'
                                   by (apply B;assumption)
    end.

这样,为了这个目标:

> Goal X->True. intros.

H:X
=====
True

more_detail. 将引入第二个假设DET:

H:X
DET:Y
DET0:Z
=====
True

并且连续调用more_detail.将失败.

然而more_detail.应始终确保,两个Y和Z …

我如何专门化泛型函数来获取指定给定类的子类的符号.例如:

(defclass a () ())
(defclass b (a) ())
(defclass c (b) ())
(defclass d () ())

(defgeneric fun (param))
(defmethod fun ((param (<subclass of> a)))
  (format t "~a is a subclass of A~%" param))

(fun 'c) ;-> "C is a subclass of A"
(fun 'd) ;-> Error: not found method for generic function call (fun 'd)

CLOS可以进行这样的调度吗？如果是的话,我应该写什么而不是" 子类 "？

比方说,我有以下结构:

/usr/bin/app
/home/me/bin/app

并$/usr/bin/app --version- - v1,$/home/me/bin/app --version- > v2.

所以,当我执行一些命令时,比如说$app --version,它会返回v1,但是我$which app给了我/home/me/bin/app,所以,我想,它必须执行第二个应用程序,然后返回v2.为什么不发生？

换句话说,结构是否$app等同于$$(which app),并且因此不适用？

如何frama-c -wp从wp手册验证示例- 一个简单的swap函数(swap.c):

/* @ requires \valid(a) && \valid(b);
   @ ensures A: *a == \old(*b);
   @ ensures B: *b == \old(*a);
   @ assigns *a,*b;
   @*/
void swap(int * a, int * b);

void swap(int * a, int * b) {
    int tmp = * a;
    *a = *b;
    *b = tmp;
    return ;
}

调用

$ frama -c -wp -wp-rte swap.c

得到:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing swap.c (with preprocessing)
[wp] Running …

我知道如何使用hunchentoot处理单个文件上传hunchentoot:post-paremter,但是当我添加一个属性时multiple,即<input name="file" type="file" multiple="multiple"/>我(hunchentoot:post-paraameter "file")只获得其中一个属性.是否存在(以及什么)接收用户选择的所有文件的机制？

通过某种方式标记所有修改的行,是否有任何方法可以就地进行当前的工作副本修改.例如,NetBeans具有以下功能:

在MSVC中,像这样的smth(不适用于VCS,但它看起来很相似): Visual Studio 2010中的绿条

我在Emacs中使用vc-mode来处理我的版本化项目.它可以计算完整的差异(vc-diff),但不方便:分别浏览差异.我希望,在文件编辑过程中知道所有更改的行.它是在某个版本控制插件中实现的吗？

证明:

Parameter A B : Prop.
Goal A->B.
intro A.

我明白了:

 1 subgoals
A : A
______________________________________(1/1)
B

我如何返回A目标部分？返回:

1 subgoals
______________________________________(1/1)
A -> B

我是一名初学 Clojure 程序员。在 Book 中，Clojure 的一个优点是不求值的代码是数据。但是我不理解。所以，我想要一个示例代码和一个解释，以便我能理解。

我是韩国人。因此，即使我写了一个尴尬的句子或未能保持我的礼貌，如果你能理解，我将不胜感激。