idris-hackers/idris-vim

strip ? from hole name before passing it to idris?

pacak opened this issue · 2 comments

pacak commented

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

Isn't this already done in #71?

pacak commented