idris-lang/Idris-dev — pull request #1428 by trillioneyes (2014-07-24 23:45:32+00:00)
Title: Improving :let

`:let` now handles many more types of declarations, including classes, instances, and fixities. Things like using and mutual blocks should also be supported, but I'm not sure how to enter them on a single line, so I haven't tested them. Syntax declarations don't work yet, but I plan to allow them soon.

There is also an `:undefine`/`:unlet` command, to remove one or more definitions given at the repl (or all such definitions, if used without an argument).

idris> :let class Hands a where hands : a
idris> :let instance Hands Nat where hands = Z
idris> the Nat hands
0
idris> :let foot = Z; feet = S Z; feeet = S (S Z)
idris> feeet
2
idris> :undefine foot feeet
idris> foot
-- error
idris> feet
1
idris> :undefine
idris> feet
-- error