在 (*1) 中可以阅读下一个
rewrite prf in expr
If we have
prf : x = y
, and the required type for expr is some property ofx
, therewrite ... in
syntax will search forx
in the required type ofexpr
and replace it withy
.
现在,我有下一段代码(你可以将它复制到编辑器并尝试 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)
。并且 prf
等于 plus y k = plus k y
其中 x
是 plus y k
和 y
是 加 k y
。而rewrite应该在expr
中搜索x
(即for plus y k
)(即S (plus y k) = plus y (S k)
并且应该将 x
替换为 y
(即用 plus k y
)。结果(res
) 应该是 S (plus k y) = plus y (S k)
。
但这行不通。
我有 idris 的下一个答案
rewriting plus y k to plus k y did not change type letty
我猜重写只是为了改变结果表达式的类型。因此,它在 let
表达式的主体内不起作用,而仅在它的“in”部分起作用。这是正确的吗?
(*1) http://docs.idris-lang.org/en/latest/proofs/patterns.html
附言。教程中的示例工作正常。我只是想知道为什么我尝试使用重写的方式不起作用。
最佳答案
虽然文档中没有明确说明,rewrite
是对 Elab
战术脚本 (defined around here) 的语法糖调用。
为什么您的示例不起作用:未找到“expr
的必需类型”;仅使用 res = rewrite prfXeqY in expr
,不清楚 res
应该具有哪种类型(甚至统一器可以用解决这个问题>let res = … in res
。)如果您指定所需的类型,它将按预期工作:
res = the (S (plus k y) = plus y (S k)) (rewrite prfXeqY in expr)
关于idris - 为什么重写在这种情况下不改变表达式的类型?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/50779105/