[4.1.3] :let vs let

[nbloomf]

I can imagine a novice reader getting confused about the difference between let and :let. I've never used Idris before, but have used Haskell for a decade, so I'll take a stab at it.

let is a gentle extension to the usual lambda calculus syntax. The expression let x = y in e is equivalent to (\x . e) y. There are a couple of good reasons for introducing this syntax. First, it makes it easy to shorten a lambda expression by factoring out common subexpressions. Second, it has nice implications for the type inference algorithm, at least in the simply typed case; IIRC there are let expressions that can be efficiently assigned a (simple) type even though the equivalent lambda form cannot.

At any rate, because let is a first-class part of the lambda expression grammar, we can do weird things like

f (let x = p a in if q then x else g x)

Not to say that deeply nested lets are the best way to define something, but you can do it.

If I understand correctly :let is different - it is just used to bind new names at the top level of an interactive Idris session. I think the equivalent Haskell idiom would be let used in the REPL, which happens to be an instance of the special let form for monads (since the haskell repl is just an iteratively defined value in IO ()).