javascript tutorial: no output

[cristipp]

I'm going through https://leanprover.github.io/tutorial. I'd expect the result of the "check" statements (which is manually added as comments) to show up somewhere upon execution. Unfortunately, it doesn't, so experimenting on my own is rather limited. There are also statements in the text that indicate I should see something, like Lean's output seems to indicates that Type is an element of itself..

All I see is:

-- Processing...
-- Saved at cookie.
-- Done(0.013sec)

[cristipp]

Oh, the types do show up. As comments in text. Since the original text already had them as comments, nothing was happening on "shift + enter".

[cristipp]

Sorry, the types didn't show up as comments. I still see no output on "shift + enter". Furthermore:

• constant f'' : \nat -> \nat doesn't type check, complains about "unexpected token".
• Unclear what \what sequence to use for the lambda symbol.

[soonhokong]

For each check command, it provides a small "i" icon on the left gutter to display a corresponding information. You can move your mouse on it to see the details. See the following screenshot.

If you want to see the output at the console pane, there is an option for that. Please click the 'gear' icon (Settings) and set the value for "Print output to console" to be true.

Then, the output should be directed to the console pane as the following screenshot.

[soonhokong]

Unclear what \what sequence to use for the lambda symbol.

There is an appendix A.1.8 which explains how to type some of the Unicode symbols in the editor.

[fpvandoorn]

@soonhokong: This seems to be a recurring question. I recommend setting this value to be true by default:

If you want to see the output at the console pane, there is an option for that. Please click the 'gear' icon (Settings) and set the value for "Print output to console" to be true.

[cristipp]

Thanks! I'm getting some output now. Regarding \lam, I'm doing something wrong in the JS console. Perhaps Emacs is doing some preprocessing that is not available in js?

[cristipp]

Here's another fun one, the result of eval 2 + 3 is somewhat harder to read than 5:

[avigad]

@cristipp Thanks for catching this.

Recently, we changed the handling of numerals in Lean. The issue is now that the numerals in "2 + 3" are interpreted as generic numerals. The metavariable expressions like "?M_1" means that the system doesn't know what type they are, and so the "evaluation" is uninformative.

We can fix this by writing, for example, (2 : nat) + 3. I will fix this tomorrow.

[cristipp]

Thanks for the eval tip. I also figured out how to type lambdas:

definition curry (A B C : Type) (f : A × B → C) : A → B → C :=
  fun a b, f (a, b)

[fpvandoorn]

\lam is not a way to input λ, you should use \fun or \l (or the ASCII variant fun). I fixed it in the Quick Reference: leanprover/tutorial#147

[cristipp]

Edit2. @fpvandoorn was kind to answer quick enough, only fair to leave the question. I was confused in the declaration of vec, why cons takes an A first argument, whereas empty and append don't. In particular, as A is already the first argument of Π.

namespace vec
  constant empty : Π A : Type, vec A 0
  constant cons : Π (A : Type) (n : nat), A → vec A n → vec A (n + 1)
  constant append : Π (A : Type) (n m : nat), vec A m → vec A n → vec A (n + m)
end vec

Edit: Ignore, figured it out.

PS. The online interactive tutorial is fantastic. I wish I had it 10 years ago :)

[fpvandoorn]

The reason is that cons is a function, which takes an element a of type A, and a vector v of type vec A n and produces a vector a :: v (prepend a to v) of type vec A (n+1).

So (for a given A and n) it is really a function A → vec A n → vec A (n + 1). The other two functions don't depend on an element a of type A (but they do depend on the type A itself).

[avigad]

@cristipp Thanks for the kind words about the tutorial! The problem described above was fixed in this pull request:

https://github.com/leanprover/tutorial/pull/148

If that looks good to you, could you close this issue?

Two small comments:

• For issues related to the tutorial, you can open issues on the tutorial repository, and then we can close them automatically with the corresponding pull requests.

• There is also a Lean user group:

  https://groups.google.com/forum/#!forum/lean-user

  Feel free to post questions there as well.

[cristipp]

@avigad. All looks great. Thanks for the pointers. Keep up the good work! About the tutorial, one thing it didn't seem to get to [or I didn't got that far] is how to harness the power of the SMT apis to create one's own automated tactics.

[avigad]

The Lean project is still new, and that kind of automation is not there yet. Leo de Moura and Daniel Selsam are working hard now on adding a tableau theorem prover and term simplifier, and SMT capabilities are further down the line. Rest assured, though, that as they become available, we'll continue to document them.