我正在查看以下面的指令开头的OCaml源文件:
open! MiscParser
我理解这open MiscParser意味着"打开MiscParser模块",但我不知道感叹号的含义.
当我在伊莎贝尔中说出一个引理时,我经常打字nitpick,如果这不能给我一个反例.然后我键入sledgehammer以尝试自动查找证明.
我想知道:是否可以调用Nitpick和Sledgehammer以便它们同时运行？由于Sledgehammer已经将我的引理发送给了许多自动证明器,这些证明器中的其中一个实际上不是像Nitpick那样的反例调查器吗？
当我apply (rule)在apply-script中使用时,通常会选择适当的规则.这同样适用于proof结构化证明.我在哪里可以学习/查找所用规则的名称？
有时,当我在写申请风格的证明,我就想办法修改论证方法 foo来
尝试
foo第一个目标.如果它解决了目标,那就好; 如果它没有解决它,恢复到原始状态并失败.
这出现在以下代码中:
qed (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)+
在进一步改变之后,调用simp将不再完全解决目标,然后这将循环.如果我可以指定类似的东西
qed (solve_goal(subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail))+
或(替代建议的synatx)
qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)!)+
或者(甚至更好的语法)
qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)[1!])+
它会停止在这个脚本无法解决的第一个目标上.
我的问题是基于Trey Jackson对SyntaxT3rr0r这个问题的回答.
Trey提出了以下函数,用于递增Emacs缓冲区的选定区域中的每个两位数字.
(defun add-1-to-2-digits (b e)
"add 1 to every 2 digit number in the region"
(interactive "r")
(goto-char b)
(while (re-search-forward "\\b[0-9][0-9]\\b" e t)
(replace-match (number-to-string (+ 1 (string-to-int (match-string 0)))))))
我想将此功能用于我自己的目的.但是,我想连续多次增加数字.该函数的当前形式的问题是,在每次调用之前,我必须用鼠标再次选择该区域.
我的问题是:如何修改Trey的功能,使其在调用后离开选定的区域？(我的最终目的是将此功能分配给键盘快捷键(类似ctrl+ ↑),这样,如果我按住ctrl和↑按键,我所选区域中的所有两位数字都会不断增加.)
顺便说一句,我知道Brian Campbell的这个答案,建议使用exchange-point-and-mark重新选择之前选择的区域.但是,我试过了,在这种情况下似乎没有帮助.
我最近开始使用xargs
提供的优秀软件包\newcommandx.它共享类似于默认语法的语法\newcommand.我想font-lock反映一下.我做到了
(custom-set-variables
'(font-latex-user-keyword-classes
(quote (("cx" ("newcommandx" "*|{\\[[{")
(:family "font-lock-type-face") command)))))
但是,这只是fontifies命令名称本身,而不是它的身体(\newcommandfontifies与身体'font-lock-function-name-face,这在我的情况是粗体).我想\newcommandx用它来塑造它的身体'font-lock-function-name-face.
总结一个问题:如何使fontification \newcommandx完全相同\newcommand(即在我的情况下是大胆的身体)？
我有一个伊莎贝尔理论文件，名为John.thy. 我想把它展示给我的朋友，但我的朋友没有 Isabelle，而且原始.thy文件不太容易阅读。我在 Isabelle 库中看到了一些网页（例如： http: //isabelle.in.tum.de/library/HOL/Finite_Set.html），它们具有漂亮的语法突出显示，我希望我的理论看起来像像那样。
那么我该如何制作呢John.html？我查看了文档，所有的构建文件和 make 文件等看起来都相当可怕和困难。有好心人可以解释一下最简单的方法吗？
假设我写了一个用于反转列表的函数.我想用value命令测试它,只是为了向自己保证我可能做对了.但输出看起来很可怕:
value "reverse [1,8,3]"
> "[1 + 1 + 1, 1 + 1 + (1 + 1) + (1 + 1 + (1 + 1)), 1]" :: "'a list"
如果我告诉Isabelle将这些数字字符视为自然,输出会更糟:
value "reverse [1::nat,8,3]"
> "[Suc (Suc (Suc 0)), Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))), Suc 0]" :: "nat list"
有时候我会求助于使用字符串,但对于所有这些撇号而言,这看起来有点滑稽:
value "reverse [''1'',''8'',''3'']"
> "[''3'', ''8'', ''1'']" :: "char list list"
我可以指示伊莎贝尔漂亮的打印机打印Suc (Suc (Suc 0))的3,等等？也许通过放弃一些神奇的咒语,syntax或translations命令？
这是我的完整示例,如果您想将其粘贴到Isabelle中:
theory …我有点意外
value "let x = SOME n. n ? {1::int,2} in x = x"
回报True.经过β扩展和α重命名后,该术语与以下内容相同:
value "(SOME na. na ? {1::int,2}) = (SOME nb. nb ? {1::int,2})"
我不明白为什么这种平等应该成立.为什么选择的值与选择的值na相同nb？
我有一个相当大的术语foo。当我打字时
value "foo"
然后 Isabelle 计算foo出一个值，例如foo_value。我现在想证明以下引理。
lemma "foo = foo_value"
我应该使用什么证明方法？我尝试过try，但超时了。我想我可以通过展开 中出现的各种定义来手动进行foo，但我肯定应该能够利用该value命令正在使用的任何机制，对吧？
这个问题涉及使用Isabelle/HOL定理证明器生成代码.
当我导出distinct列表上的函数的代码时
export_code distinct in Scala file -
我得到以下代码
def member[A : HOL.equal](x0: List[A], y: A): Boolean = (x0, y) match {
case (Nil, y) => false
case (x :: xs, y) => HOL.eq[A](x, y) || member[A](xs, y)
}
def distinct[A : HOL.equal](x0: List[A]): Boolean = x0 match {
case Nil => true
case x :: xs => ! (member[A](xs, x)) && distinct[A](xs)
}
此代码具有二次运行时.有更快的版本吗？我想到了"~~/src/HOL/Library/Code_Char"在我的理论开头导入字符串并建立列表的高效代码生成之类的东西.更好的实现distinct方法是在O(n log n)中对列表进行排序,并迭代列表一次.但我猜一个人可以做得更好吗？
无论如何,是否有更快的实现distinct和可能的其他功能Main？