SpaceVim

A community-driven vim distribution


主页 | 关于我们 | 使用文档 | 开发指南 | 用户社区 | 赞助


可用模块 » lang#idris

模块简介

这一模块为在 SpaceVim 中进行 idris 开发提供了支持,该模块主要基于插件:wsdjeg/vim-idris

启用模块

可通过在配置文件内加入如下配置来启用该模块:

[[layers]]
  name = "lang#idris"

快捷键

快捷键 功能描述
SPC l a 重新载入当前文件
SPC l w add with clause
SPC l t 显示光标变量类型
SPC l p proof search
SPC l o obvious proof search
SPC l c case split
SPC l f refine item
SPC l l make lemma
SPC l m add missing
SPC l h 显示光标函数文档
SPC l e idris 求值
SPC l i 打开应答窗口

交互式编程

启动 idris --nobanner 交互进程,快捷键为: SPC l s i

将代码传输给 REPL 进程执行:

快捷键 功能描述
SPC l s b 发送整个文件内容至 REPL
SPC l s l 发送当前行内容至 REPL
SPC l s s 发送已选中的内容至 REPL

运行当前脚本

在编辑 idris 文件时,可通过快捷键 SPC l r 快速异步运行当前文件,运行结果会展示在一个独立的执行窗口内。

网站源码位于 Github, 帮助改进本页面 — 网站主题: mattgraham,