/language-agda

Agda language support for the Atom editor

MIT LicenseMIT

language-agda package

Adds syntax highlighting to Agda files in Atom.

Contributions are greatly appreciated. Please fork this repository and open an pull request to add snippets, make grammar tweaks, etc.

Snippets

with-abstraction

Whenever you need a with-abstraction

filter : {A : Set} → (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) $1 = ?

Simply type with at the $1 position before = ? and then press tab or enter, the snippet would set up a scaffolding with cursor positioned at$1, press tab to jump the cursor from $1 to $2.

filter : {A : Set} → (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) with $1
... | $2 = ?

(in)equational-reasoning

eq for this:

begin
    {! $1 !}
≡⟨ {!   !} ⟩
    {!   !}
≡⟨ {!   !} ⟩
    {!   !}
≡⟨ {!   !} ⟩
    {!   !}
≡⟨ {!   !} ⟩
    {!   !}
∎

eqs for a small step:

≡⟨ {! $1 !} ⟩
    {!   !}

po for this:

start
    {!  !}
≤⟨ {!   !} ⟩
    {!   !}
≤⟨ {!   !} ⟩
    {!   !}
≤⟨ {!   !} ⟩
    {!   !}
≤⟨ {!   !} ⟩
    {!   !}
□

note that the operators of pre-order reasoning are renamed to prevent conflicts with equational reasoning

open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)

also pos for a small step:

≤⟨ {!  !} ⟩
    {!   !}

px and pxs in case you have reflexive relations in pre-order reasoing:

start
    {!  !}
≈⟨ {!   !} ⟩
    {!   !}
≈⟨ {!   !} ⟩
    {!   !}
≈⟨ {!   !} ⟩
    {!   !}
≈⟨ {!   !} ⟩
    {!   !}
□

How to contribute

  1. clone the repo and load it as a development package
  2. open the repo in the development mode
apm develop language-agda
atom -d ~/github/language-agda