Использование перезаписи в REPL - PullRequest
Новая
       8

Использование перезаписи в REPL

8 голосов
/ 14 мая 2019

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

...