coq - Coq：展开棘手的符号

Question

假设我想转换~X为X -> False使用unfold策略。

我有两种选择： byunfold not或 by unfold "~"。第二种方法显然更方便，因为不需要记住符号后面的定义名称。

但是，在更复杂的情况下，我没有设法做到这一点：

Definition assn_sub X a P : Assertion :=
  fun (st : state) =>
    P (X !-> aeval st a ; st).

Notation "P [ X |-> a ]" := (assn_sub X a P)
  (at level 10, X at next level).

我想在表达中展开它

((fun st0 : state => st0 Y = st0 X + st0 Z) [Z |-> Y - X]) st

不使用assn_sub. 可能吗？

标签： coq

Answer 1

带有下划线，它似乎工作。

unfold "_ [ _ |-> _ ]".