假设我想要一种策略来一次清除多个假设，做类似clear_multiple H1, H2, H3.. 我尝试使用对来做到这一点，如下所示：
Ltac clear_multiple arg :=
match arg with
| (?f, ?s) => clear s; clear_multiple f
| ?f => clear f
end.
但是，问题是我必须放置括号才能有一个Prod：
Variable A: Prop.
Goal A -> A -> A -> True.
intros.
clear_multiple (H, H0, H1).
我的问题是，如何在不使用Prods 的情况下做到这一点？
我检查了这个问题，但这不是我想要的，因为我想要的参数数量未知。
考虑以下修复点:
Require Import Coq.Lists.List.
Import ListNotations.
Inductive my_type: Type:=
| Left: my_type
| Right: my_type
.
Fixpoint decrease (which: my_type) (left right: list my_type) : list my_type :=
match which with
| Left =>
match left with
| [] => []
| a::tl => decrease a tl right
end
| Right =>
match right with
| [] => []
| a::tl => decrease a left tl
end
end.
Coq拒绝以下修复点,因为它无法猜测减少的修复点(有时候left列表会失去它的头部,有时候它就是那个right).
这个答案表明,人们可以通过使用Program Fixpoint和指定一个来解决这个问题{measure …
我正在写一个我计划发布的板条箱。发布时，最重要的事情之一（在我看来）是确保 crate 有据可查。因此我的问题是：是否有一个警告被打开，它会加热代码的未记录部分？
例如：我通常会想到类似的东西#[warn(undocumented)]。
说我有以下关系：
Inductive my_relation: nat -> Prop :=
constr n: my_relation n.
我想证明以下几点：
Lemma example:
(forall n, my_relation n -> my_relation (S n)) -> (exists n, my_relation n) -> exists n, my_relation (S n).
Proof.
intros.
介绍之后，我具有以下环境：
1 subgoal
H : forall n : nat, my_relation n -> my_relation (S n)
H0 : exists n : nat, my_relation n
______________________________________(1/1)
exists n : nat, my_relation (S n)
我的问题是：是否有可能在存在量词下重写H？如果不是，是否有解决此类问题的策略（该特定问题并非真正相关，但是存在的问题是您必须证明exists使用另一种问题exists，并且在非正式情况下可以“推论”一种方法来重写该问题）exists。假设进入exists目标）？
例如，如果尝试尝试rewrite H in H0. …
我刚刚遇到了这个“问题”：有没有一种聪明的方法可以在字符串中插入文件结尾（ASCII 0）字符？
我所说的“智能”是指比
let s = "foo" ^ (String.make 1 (Char.chr 0))
let s = "foo\000"
也就是说，这反映了我们添加的是 EOF，而不是“ascii 值为 0 的神秘字符”。
编辑：嗯...确实我在搞乱 eof 作为一个字符。但无论如何，在 C 中你可以有
#include <stdio.h>
int main(void)
{
char a = getchar();
if (a = EOF)
printf("eof");
else
printf("not eof");
return 0;
}
您可以在其中测试 char 是否是 EOF （并且(int) EOF是-1，而不是0我想的那样）。同样，您可以将 char 设置为 EOF 等。
我的问题是： ocaml 中是否有可能有类似的东西？