Define Variables in REPL

[Kevin Meredith]

In Haskell, I can define an immutable variable and function in the REPL:

λ: let x = 100 :: Int

λ: let f = \y -> y + 100

λ: f x

200

How can I do the equivalent in Idris?

[Echo Nolan]

Hi Kevin. You want the :let command. I wrote a longer response that Google Inbox ate, but the 'the' function is used instead of Haskell's :: operator. And the defaulting rules will use Integer over Int, so if you want Ints you'll need to use the both times.

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Kevin Meredith]

Thanks, Echo, that worked:

> let y = 6 in 6

> :let condition = False

> condition

False : Bool

Understood that :let is what's used to set a variable. However, what's the meaning of let:

> let y = 6 in 6

6 : Integer

> y

No such variable y

[Echo Nolan]

:let is used in the REPL, let ... in ... is used in expressions. Inside the REPL, the difference is that :let creates a variable that is bound until the end of the session or you use :unlet and the expression version only binds the variables inside the expression after in. In foo.idris source files, there is no :let.

Hope that helps :)