在REPL中使用重写

Question

对于Idris的类型驱动开发中的一项练习，我写了以下内容：

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = rewrite plusZeroRightNeutral m in Refl
myPlusCommutes (S n) m =
    rewrite myPlusCommutes n m in
      rewrite plusSuccRightSucc m n in Refl

然后我想rewrite在REPL中玩转，这样我就可以“看到”幕后发生的事情。我认为以下方法可能会起作用，但事实并非如此。

??> :let m : Nat
defined
??> :let s : (plus 0 m = plus m 0)
defined
??> rewrite plusZeroRightNeutral m in s
rewriting plus m 0 to m did not change type iType

是否可以查看rewrite使用REPL的情况？

Answer 1

rewrite x in y不会更改 的类型y以匹配预期类型，而是更改预期类型以匹配y。Idris 不知道预期的类型是什么，因为您尚未提供它。