时间戳

首页 > 解决方案 > 如何在 coq api 中获取命名目标的名称

ocaml - 如何在 coq api 中获取命名目标的名称

问题描述

我目前正在开发一个 ocaml 程序，该程序将使用 coq api 来提取有关证明及其目标的信息。为此，当使用“refine ?[name]”或其他命名目标的策略时，我想提取给目标的名称。到目前为止，我正在获得当前的目标，使用我当前的证明状态来提取它们，如下所示

(*currstate is the current state of the proof*)
let pstate = match currentstate.proof with
  | None ->
    begin
      failwith ""
    end
  | Some pst -> pst
in
let goals = (Proof.data pstate).goals in
...

使用这种方法，我可以提取目标的 ID，但不能提取它们的名称。

有没有可能提取名称？

标签： ocamlcoqcoq-plugin

解决方案

我终于找到了一种从 API 中检索命名目标名称的方法。因为我可能不是唯一需要这个的人，所以我发布了一个答案。

已经有一个功能可以让您在打印机中打印目标的名称，但遗憾的是它是私有的，不能使用。它用于Names.Id.print (Termops.evar_suggested_name goal sigma)检索名称，其中 goal 是 type Goal.goal， sigma 是 type Evd.evar_map。

推荐阅读