search

idris-hackers / idris-vim

Idris mode for vim
221 stars 52 forks source link

strip ? from hole name before passing it to idris? #74

Closed pacak closed 7 years ago

pacak commented 7 years ago

It seems like in order to make lemmas and some other things to work we need to cut of ?.

  if word =~ '^?'
    " Cut off '?' that introduces a hole identifier.
    let word = strpart(word, 1)
  endif

Before \l on hole dies with "invalid command":

plus_commutes Z m = ?plus_commutes_rhs_4

After above mentioned snippet is added \l produces

plus_commutes_rhs_4 : m = plus m 0
dkasak commented 7 years ago

Isn't this already done in #71?

pacak commented 7 years ago

You right. I cloned the repo before 74 was merged. It took some time to figure out the problem. This issue can be closed.

On Jun 4, 2017 20:08, "Denis Kasak" notifications@github.com wrote:

Isn't this already done in #71 https://github.com/idris-hackers/idris-vim/pull/71?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/idris-hackers/idris-vim/issues/74#issuecomment-306036179, or mute the thread https://github.com/notifications/unsubscribe-auth/AAECo4suPa5i6rCdZRD7D51Yr4M3BgBsks5sAp46gaJpZM4Nq-5x .