How do the lambdas?
A readonly editor is readonly. Its content is evaluated when page loads or so. Mostly for adding definitions to toplevel so they can be used later in the post:
In the regular editors we can do stuff.
Normal text-editor-stuff should work. Lambdastuff in addition:
- ctrl+l inserts a λ (or can use \ instead of λ if want to)
- ctrl+d inserts a ≜ (or can use := instead of ≜ if want to)
- ctrl+enter is used to add a definition to toplevel, or remove a definition, or do one step of evaluation
- ctrl+shift+enter is used to do like a bunch of evaluation (stops when the term is on normal form, or after like a thousand steps of evaluation)
- ctrl+r is used to replace the names used in toplevel definitions with terms from the definitions
- right-clicking within editor and selecting “Show definitions” prints all the current toplevel defintions in the editor.
ctrl+enter, ctrl+shift+enter and ctrl+r all work on the line the cursor is on. Results are printed on new line(s), after. (And cursor moves to end of result.)
So, normally, if we have written some term that maybe uses some of the toplevel defintions, we do ctrl+r and then either ctrl+enter a few times, or ctrl+shift+enter once. Can try:
Lines with ≜ (or := are for definitons). ctrl+enter on a line that goes like <identifier> ≜ <term> adds a definition.
(Most characters can be used in identifiers. Just, not whitespace ones, and not the ones that are used for other stuff: :, \, ≜, λ, ., (, ).)
The terms used in definitions can use the names of defintions that already exist. Like, we can define 2 like this now, as long as we have defined 0 and S first: (ctrl+enter)
(We can evaluate it to check that the result looks reasonably twoish. Two applications of f is very two-like, so the result should look like λf.λx.f (f x). (ctrl+r, then ctrl+shift+enter))
If we wanna get rid of a definition we can do <identifier> ≜ :(, or just <identifier> ≜. We’ll remove ω (it’s scary): (ctrl+enter)
If we try to evaluate the thing we did earler, we won’t get the same result now, since ω will just be treated as some free variable... (ctrl+r, then ctrl+shift+enter)
That’s like more or less it. In posts like this it’s mostly enough to do ctrl+enter on definitions, and ctrl+r and then ctrl+shift+enter on other stuff...