为什么在这种情况下重写不改变表达式的类型？

在(*1)中可以阅读下一篇

rewrite prf in expr

如果我们有prf : x = y，并且 expr 所需的类型是以下属性x, the rewrite ... in语法将搜索x在所需的类型中expr并将其替换为y.

现在，我有下一段代码（您可以将其复制到编辑器并尝试 ctrl-l）

module Test

plusCommZ : y = plus y 0
plusCommZ {y = Z} = Refl
plusCommZ {y = (S k)} = cong $ plusCommZ {y = k}

plusCommS : S (plus y k) = plus y (S k)
plusCommS {y = Z} = Refl
plusCommS {y = (S j)} {k} = let ih = plusCommS {y=j} {k=k} in cong ih

plusComm : (x, y : Nat) -> plus x y = plus y x
plusComm Z y = plusCommZ
plusComm (S k) y =
  let
    ih = plusComm k y
    prfXeqY = sym ih
    expr = plusCommS {k=k} {y=y}
    -- res = rewrite prfXeqY in expr
  in ?hole

下面是洞的样子

- + Test.hole [P]
 `--          k : Nat
              y : Nat
             ih : plus k y = plus y k
        prfXeqY : plus y k = plus k y
           expr : S (plus y k) = plus y (S k)
     -----------------------------------------
      Test.hole : S (plus k y) = plus y (S k)

问题。在我看来就像expr（来自*1）注释行中等于S (plus y k) = plus y (S k). And prf等于plus y k = plus k y where x is plus y k and y is plus k y。重写应该搜索x（即对于plus y k) in expr（即S (plus y k) = plus y (S k)并且应该替换x with y（即与plus k y）。和结果（res） 应该S (plus k y) = plus y (S k).

但这是行不通的。

我有伊德里斯的下一个回答

将 plus y k 重写为 plus k y 并没有改变 letty 类型

我猜重写只是为了改变结果表达式的类型。所以，它在体内不起作用let表达，但仅限于它的“in”部分。它是否正确？

(*1) http://docs.idris-lang.org/en/latest/proofs/patterns.html http://docs.idris-lang.org/en/latest/proofs/patterns.html

附言。教程中的示例效果很好。我只是想知道为什么我尝试使用重写的方法不起作用。

尽管文档中没有明确说明，rewrite是语法糖调用Elab战术脚本（定义在此处 https://github.com/idris-lang/Idris-dev/blob/f92ecd25d48a9120abfbb7d6af81f9b194ab98f1/src/Idris/Elab/Rewrite.hs).

为什么你的例子不起作用：“所需的类型expr“ 未找到；仅res = rewrite prfXeqY in expr单独来看，不清楚是哪种类型res应该有（甚至统一者could解决这个问题let res = … in res.) 如果您指定所需的类型，它将按预期工作：

res = the (S (plus k y) = plus y (S k)) (rewrite prfXeqY in expr)