coq - 如何从归纳类型 Coq 中获取数据

Question

我对 Coq 有点陌生，我正在尝试对 Coq 中的常规语法进行一些形式化。假设我有一个归纳类型如下：

Inductive rules : non_terminal -> list(non_terminal + terminal) -> Type :=
  rule1 : rules S [inr a; inl S] 
| rule2 : rules S [inr b;inl S] 
| rule3 : rules S [].

代表(a* b*)语法的推导规则。假设我想提取它们以供以后使用。有什么办法可以做到这一点并将其存储在列表列表中？例如，我想要一个可以返回 me 的程序[[S [inr a; inl S];S [inr b;inl S];[]]。任何其他想法将不胜感激。

提前致谢。

Answer 1

您可以尝试使用 Ltac2，它可以以编程方式获取有关归纳类型的信息？你也可以使用 template-coq 包/插件。不过，这些可能实际上并不是您想要在这里做的，因为它有点令人费解。