Skip to main content Svelte Highlight v7.21.1

Agda language preview

1. Naturals and a simple proof

a unicode data declaration and a recursive function
horizon-dark
{-# OPTIONS --safe #-}
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))
atom-one-dark
{-# OPTIONS --safe #-}
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))
github-dark
{-# OPTIONS --safe #-}
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))
dracula
{-# OPTIONS --safe #-}
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))
nord
{-# OPTIONS --safe #-}
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))
github
{-# OPTIONS --safe #-}
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))

2. Records and modules

a record type and a module namespace
horizon-dark
record Point : Set where
  field
    x : ℕ
    y : ℕ

module Origin where
  origin : Point
  origin = record { x = zero ; y = zero }
atom-one-dark
record Point : Set where
  field
    x : ℕ
    y : ℕ

module Origin where
  origin : Point
  origin = record { x = zero ; y = zero }
github-dark
record Point : Set where
  field
    x : ℕ
    y : ℕ

module Origin where
  origin : Point
  origin = record { x = zero ; y = zero }
dracula
record Point : Set where
  field
    x : ℕ
    y : ℕ

module Origin where
  origin : Point
  origin = record { x = zero ; y = zero }
nord
record Point : Set where
  field
    x : ℕ
    y : ℕ

module Origin where
  origin : Point
  origin = record { x = zero ; y = zero }
github
record Point : Set where
  field
    x : ℕ
    y : ℕ

module Origin where
  origin : Point
  origin = record { x = zero ; y = zero }

3. Nested comments

a comment wrapping an example that has its own comment
horizon-dark
{- doubles a natural number
   {- example: double 21 ≡ 42 -}
-}
double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))
atom-one-dark
{- doubles a natural number
   {- example: double 21 ≡ 42 -}
-}
double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))
github-dark
{- doubles a natural number
   {- example: double 21 ≡ 42 -}
-}
double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))
dracula
{- doubles a natural number
   {- example: double 21 ≡ 42 -}
-}
double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))
nord
{- doubles a natural number
   {- example: double 21 ≡ 42 -}
-}
double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))
github
{- doubles a natural number
   {- example: double 21 ≡ 42 -}
-}
double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))