show type

Open arademaker opened this issue 7 years ago • 1 comments

http://leanprover.github.io/presentations/20150123_lean-mode/lean-mode.pdf

slide 5 says I can have a type of a subterm if I put a cursor on the open-paren. it is not working for me. Any idea?

Emacs 26.1. MacOS 10.14,

$ lean -version Lean (version 3.4.1, Release)

package installed via MELPA.

Oct 25 '18 12:10 arademaker

This was a feature of Lean 2 that did not survive the change to the new server infrastructure in Lean 3. It may be easier to bring it back in Lean 4 in the future.

Oct 25 '18 12:10 Kha