![]() For instance, parentheses are required in #eval String.append "great " (String.append "oak " "tree")īecause otherwise the second String.append would be interpreted asĪn argument to the first, rather than as a function being passed Necessary when a function's argument is to be computed via anotherįunction call. Parentheses in the expression (1 + 2) * 5, parentheses are also Just as the order-of-operations rules for arithmetic demand Where the function's two arguments are simply written next to One would instead write #eval String.append "Hello, " "Lean!" Rather than writing #eval String.append("Hello, ", "Lean!") Function application is one of the most common operations, f(x)) to apply a function to itsĪrguments, Lean simply writes the function next to itsĪrguments (e.g. Programming languages use parentheses (e.g. While both ordinary mathematical notation and the majority of Lean obeys the ordinary rules of precedence and associativity forĪrithmetic operators. Is found by putting the cursor or mouse pointer over #eval. To ask Lean to evaluate an expression, write #eval before it in yourĮditor, which will then report the result back. Thus, this chapter focuses on how toĮvaluate expressions interactively with Lean, while the next chapterĭescribes how to write, compile, and run the Hello, world! program. ![]() Not mean that Lean cannot be used to write Hello, world! to theĬonsole, but performing I/O is not a core part of the experience of Will not cause the program to compute a different result. If twoĮxpressions have the same value, then replacing one with the other Evaluating an expression cannot have side effects. Once given a value, variables cannot be reassigned. In Lean, however, programs work the same way as mathematicalĮxpressions. Model of evaluating mathematical expressions. "Side effects" is essentially a catch-all term forĭescribing things that may happen in a program that don't follow the Throwing or catching exceptions, and reading data from aĭatabase. In addition to mutable state, programs may have other sideĮffects, such as deleting files, making outgoing network connections, Value referred to by a variable can change over time. Programs have access to mutable memory, so the Of a series of statements that should be carried out in order to find Most programming languages are imperative, where a program consists In Lean, programs are first and foremost expressions, and the primary way to think about computation is as evaluating expressions to find their values. Sometimes, mathematical expressions contain variables: the value of x + 1 cannot be computed until we know what the value of x is. To find the value of the latter expression, 3 + 1 is first replaced by 4, yielding 2 × 4, which itself can be reduced to 8. The value of 15 - 6 is 9 and the value of 2 × (3 + 1) is 8. Value of an expression, just as one does in arithmetic. The most important thing to understand as a programmer learning Lean Interlude: Tactics, Induction, and Proofs Pitfalls of Programming with Dependent Types Functors, Applicative Functors, and Monads Interlude: Propositions, Proofs, and Indexing
0 Comments
Leave a Reply. |