Menu
For one of the exercises in Type-Driven Development with Idris, I wrote the following:
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
Then I wanted to play around with rewrite in the REPL, so I could "see" what was happening behind the scenes. I thought the following might work, but it didn't.
λΠ> :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
Is it possible to see what rewrite is doing using the REPL?
922
Type the :paste command in the REPL. Paste in your block of code (Command-V on a Mac, Ctrl-V on Windows). Press Ctrl-D, and the REPL will evaluate what you pasted in.
Click the "Share" button near the top-right of the repl: In the box that appears, click "Copy" to copy the multiplayer link. You can share that link with your partner (for example, by pasting it into the chat window in Zoom).
Running code from Replit's REPL You can type code in the right-hand pane (pane 3) and press the "Enter" key to run it.
This Repl is a Flask app that can say "Hello World" in 5 different languages, and it's ready to get published. To publish, press the publish button in the top right corner of the Workspace.
rewrite x in y does not change the type of y to match the expected type, it change the expected type to match y. Idris does not know what the expected type is because you have not provided it.
182
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
