search

aya-prover / aya-vscode

~ VSCode extension for Aya Prover
GNU General Public License v3.0
7 stars 2 forks source link

Can’t go to definition when the cursor is at the right side of a term #8

Open by-cloud opened 3 years ago

by-cloud commented 3 years ago

VSCode shows notifications like “No definition found for ‘suc’”.

ice1000 commented 3 years ago

https://github.com/aya-prover/aya-dev/blob/de31e4fbaed2c699ee56b068e484abaa42e89199/api/src/main/java/org/aya/api/error/SourcePos.java#L90

Does changing the above column <= endColumn to column + 1 <= endColumn solve the problem

imkiva commented 3 years ago

I cannot reproduce the problem. Can you describe what you did?

ice1000 commented 3 years ago

Maybe putting the cursor at suc<cursor> and press the shortcut for goto def

ice1000 commented 3 years ago

Not by ctrl+clicking