Для одного из упражнений в Type-Driven Development с 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?