代码之家 › 专栏 › 技术社区 › Bromind

可变arity策略

ltac variadic coq

5

Bromind · 技术社区 · 8 年前

假设我想有一个策略,一次清除多个假设,做一些类似的事情 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).

我的问题是,如何不使用 戳 s

我检查过了 this question ,但这并不完全是我想要的,因为我想要的参数数量未知。

1 回复 | 直到 8 年前

1

4

Arthur Azevedo De Amorim 8 年前

你可能想知道 clear 策略可以接受多个参数,所以您不需要定义新的策略:您只需编写 clear H H0 H1 .

当然,您可能希望为其他任务定义这样的n元策略。Coq有一个 tactic notation mechanism 这支持这样的定义。不幸的是,它们并不太强大:您只能将某种类型的参数列表传递给需要多个参数的策略(例如 清楚的 ); 我认为它不能提供一个可以通过编程进行迭代的列表。