search

idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
269 stars 71 forks source link

display in browse isn't taking the implicitness into account #422

Closed jasonhemann closed 7 years ago

jasonhemann commented 8 years ago

When I look up weakenN from the Fin library (via apropos) I get an expected type. Yet when I browse the namespace I get a different, though seemingly also reasonable type. I thought that perhaps the definition had been changed to the latter, but it seems the former is still correct. @david-christiansen , you mentioned that the display in browse isn't taking the implicitness into account. I attach an image below.

bug

david-christiansen commented 8 years ago

Confirmed. For comparison, the :browse at the REPL does what it should.

david-christiansen commented 8 years ago

Though this is actually a bug in Idris itself, rather than the Emacs mode.

david-christiansen commented 7 years ago

This is working for me now, so I think someone fixed it. How about you?

david-christiansen commented 7 years ago

Please re-open if it's still an issue for you.