search

leanprover / lean3-mode

Emacs mode for Lean
Apache License 2.0
69 stars 17 forks source link

show type #12

Open arademaker opened 6 years ago

arademaker commented 6 years ago

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.

Kha commented 6 years ago

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.