Welcome!

jekyll-agda is a Jekyll plugin to write websites using literate Agda.

This is a demo page; for more information please refer to the documentation.

Let’s define Peano’s natural numbers:

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

Cool! Now let’s define addition inductively:

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

Note that ℕ, zero and suc are hyperlinked to their definition above.

As our last trick, let’s import some tools for equational reasoning and check that 2 + 2 is indeed 4.

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

{-# BUILTIN NATURAL ℕ #-}

_ :  +  ≡ 
_ = begin
   +                                  ≡⟨⟩
  (suc (suc zero)) + (suc (suc zero))   ≡⟨⟩
  suc ((suc zero) + (suc (suc zero)))   ≡⟨⟩
  suc (suc (zero + (suc (suc zero))))   ≡⟨⟩
  suc (suc (suc (suc zero)))            ≡⟨⟩
                                       ∎

Note that all imported modules, keywords and operators are hyperlinked to their definition in the standard library. Try jumping into the rabbit hole and navigate around it!

This concludes the demonstration.

I hope jekyll-agda can help you. ❤️