search

derekelkins / agda-vim

Agda interaction in vim
BSD 2-Clause "Simplified" License
130 stars 47 forks source link

Unknown function: AgdaMakeCase #55

Closed VDVinh closed 4 years ago

VDVinh commented 4 years ago

Sorry, I got the error: Unknown function: AgdaMakeCase while type: \c May I know where can I find this function ?

derekelkins commented 4 years ago

This is defined in the agda.py file. It seems your version of vim supports Python but failed to load agda.py. It's hard to provide more help without more information. What OS are you running this under? What version of vim? Are you using a vim package manager? If so which one? Does your version support Python 2? Were there any error messages when you loaded an Agda file? They may be on the console after you close vim. Do you have the agda.py file?

VDVinh commented 4 years ago

Thanks for your reply and detailed explanations for helping. You are correct. My vim do not support python, it supports python3 only. I solved by adding python to my vim.