Some checks failed
Detach Plugins / check (FlyGrep.vim) (push) Has been cancelled
Detach Plugins / check (GitHub.vim) (push) Has been cancelled
Detach Plugins / check (JavaUnit.vim) (push) Has been cancelled
Detach Plugins / check (SourceCounter.vim) (push) Has been cancelled
Detach Plugins / check (cpicker.nvim) (push) Has been cancelled
Detach Plugins / check (dein-ui.vim) (push) Has been cancelled
Detach Plugins / check (git.vim) (push) Has been cancelled
Detach Plugins / check (iedit.vim) (push) Has been cancelled
Detach Plugins / check (scrollbar.vim) (push) Has been cancelled
Detach Plugins / check (vim-chat) (push) Has been cancelled
Detach Plugins / check (vim-cheat) (push) Has been cancelled
Detach Plugins / check (vim-todo) (push) Has been cancelled
Detach Plugins / check (xmake.vim) (push) Has been cancelled
test / Linux (nvim, nightly) (push) Has been cancelled
test / Linux (nvim, v0.3.8) (push) Has been cancelled
test / Linux (nvim, v0.4.0) (push) Has been cancelled
test / Linux (nvim, v0.4.2) (push) Has been cancelled
test / Linux (nvim, v0.4.3) (push) Has been cancelled
test / Linux (nvim, v0.4.4) (push) Has been cancelled
test / Linux (nvim, v0.5.0) (push) Has been cancelled
test / Linux (nvim, v0.5.1) (push) Has been cancelled
test / Linux (nvim, v0.6.0) (push) Has been cancelled
test / Linux (nvim, v0.6.1) (push) Has been cancelled
test / Linux (nvim, v0.7.0) (push) Has been cancelled
test / Linux (nvim, v0.7.2) (push) Has been cancelled
test / Linux (nvim, v0.8.0) (push) Has been cancelled
test / Linux (nvim, v0.8.1) (push) Has been cancelled
test / Linux (nvim, v0.8.2) (push) Has been cancelled
test / Linux (nvim, v0.8.3) (push) Has been cancelled
test / Linux (nvim, v0.9.0) (push) Has been cancelled
test / Linux (nvim, v0.9.1) (push) Has been cancelled
test / Linux (true, vim, v7.4.052) (push) Has been cancelled
test / Linux (true, vim, v7.4.1689) (push) Has been cancelled
test / Linux (true, vim, v7.4.629) (push) Has been cancelled
test / Linux (true, vim, v8.0.0027) (push) Has been cancelled
test / Linux (true, vim, v8.0.0183) (push) Has been cancelled
test / Linux (vim, nightly) (push) Has been cancelled
test / Linux (vim, v8.0.0184) (push) Has been cancelled
test / Linux (vim, v8.0.1453) (push) Has been cancelled
test / Linux (vim, v8.1.2269) (push) Has been cancelled
test / Linux (vim, v8.2.2434) (push) Has been cancelled
test / Linux (vim, v8.2.3995) (push) Has been cancelled
test / Windows (nvim, nightly) (push) Has been cancelled
test / Windows (nvim, v0.3.8) (push) Has been cancelled
test / Windows (nvim, v0.4.2) (push) Has been cancelled
test / Windows (nvim, v0.4.3) (push) Has been cancelled
test / Windows (nvim, v0.4.4) (push) Has been cancelled
test / Windows (nvim, v0.5.0) (push) Has been cancelled
test / Windows (nvim, v0.5.1) (push) Has been cancelled
test / Windows (nvim, v0.6.0) (push) Has been cancelled
test / Windows (nvim, v0.6.1) (push) Has been cancelled
test / Windows (nvim, v0.7.0) (push) Has been cancelled
test / Windows (nvim, v0.7.2) (push) Has been cancelled
test / Windows (nvim, v0.8.0) (push) Has been cancelled
test / Windows (nvim, v0.8.1) (push) Has been cancelled
test / Windows (nvim, v0.8.2) (push) Has been cancelled
test / Windows (nvim, v0.8.3) (push) Has been cancelled
test / Windows (nvim, v0.9.0) (push) Has been cancelled
test / Windows (nvim, v0.9.1) (push) Has been cancelled
test / Windows (vim, nightly) (push) Has been cancelled
test / Windows (vim, v7.4.1185) (push) Has been cancelled
test / Windows (vim, v7.4.1689) (push) Has been cancelled
test / Windows (vim, v8.0.0027) (push) Has been cancelled
test / Windows (vim, v8.0.1453) (push) Has been cancelled
test / Windows (vim, v8.1.2269) (push) Has been cancelled
test / Windows (vim, v8.2.2434) (push) Has been cancelled
test / Windows (vim, v8.2.3995) (push) Has been cancelled
docker / docker (push) Has been cancelled
mirror / check (coding) (push) Has been cancelled
mirror / check (gitee) (push) Has been cancelled
mirror / check (gitlab) (push) Has been cancelled
54 lines
1.4 KiB
Markdown
54 lines
1.4 KiB
Markdown
---
|
|
title: "SpaceVim lang#agda layer"
|
|
description: "This layer adds Agda language support to SpaceVim."
|
|
---
|
|
|
|
# [Available Layers](../../) >> lang#agda
|
|
|
|
<!-- vim-markdown-toc GFM -->
|
|
|
|
- [Description](#description)
|
|
- [Features](#features)
|
|
- [Install](#install)
|
|
- [Key bindings](#key-bindings)
|
|
|
|
<!-- vim-markdown-toc -->
|
|
|
|
## Description
|
|
|
|
Agda is a dependently typed functional programming language.
|
|
This layer adds [Agda](https://github.com/agda/agda) language support to SpaceVim.
|
|
|
|
## Features
|
|
|
|
- syntax highlighting
|
|
|
|
## Install
|
|
|
|
To use this configuration layer, update your custom configuration file with:
|
|
|
|
```toml
|
|
[[layers]]
|
|
name = "lang#agda"
|
|
```
|
|
|
|
## Key bindings
|
|
|
|
| Key bindings | Description |
|
|
| ------------ | ------------------------ |
|
|
| `SPC l r` | execute current file |
|
|
| `SPC l l` | reload |
|
|
| `SPC l t` | infer |
|
|
| `SPC l f` | refine false |
|
|
| `SPC l F` | refine true |
|
|
| `SPC l g` | give |
|
|
| `SPC l c` | make case |
|
|
| `SPC l a` | auto |
|
|
| `SPC l e` | context |
|
|
| `SPC l n` | Normalize IgnoreAbstract |
|
|
| `SPC l N` | Normalize DefaultCompute |
|
|
| `SPC l M` | Show module |
|
|
| `SPC l y` | why in scope |
|
|
| `SPC l h` | helper function |
|
|
| `SPC l m` | metas |
|