Skip to main content Svelte Highlight v7.21.1

Lean language preview

1. A theorem with unicode operators

∀, →, and ℕ in a type signature and proof
horizon-dark
def succ (n : ℕ) : ℕ := n + 1

theorem succ_pos : ∀ n : ℕ, succ n > 0 := by
  intro n
  simp [succ]
atom-one-dark
def succ (n : ℕ) : ℕ := n + 1

theorem succ_pos : ∀ n : ℕ, succ n > 0 := by
  intro n
  simp [succ]
github-dark
def succ (n : ℕ) : ℕ := n + 1

theorem succ_pos : ∀ n : ℕ, succ n > 0 := by
  intro n
  simp [succ]
dracula
def succ (n : ℕ) : ℕ := n + 1

theorem succ_pos : ∀ n : ℕ, succ n > 0 := by
  intro n
  simp [succ]
nord
def succ (n : ℕ) : ℕ := n + 1

theorem succ_pos : ∀ n : ℕ, succ n > 0 := by
  intro n
  simp [succ]
github
def succ (n : ℕ) : ℕ := n + 1

theorem succ_pos : ∀ n : ℕ, succ n > 0 := by
  intro n
  simp [succ]

2. Structures and namespaces

structure, namespace, and a def inside it
horizon-dark
structure Point where
  x : ℤ
  y : ℤ

namespace Point

def origin : Point := { x := 0, y := 0 }

end Point
atom-one-dark
structure Point where
  x : ℤ
  y : ℤ

namespace Point

def origin : Point := { x := 0, y := 0 }

end Point
github-dark
structure Point where
  x : ℤ
  y : ℤ

namespace Point

def origin : Point := { x := 0, y := 0 }

end Point
dracula
structure Point where
  x : ℤ
  y : ℤ

namespace Point

def origin : Point := { x := 0, y := 0 }

end Point
nord
structure Point where
  x : ℤ
  y : ℤ

namespace Point

def origin : Point := { x := 0, y := 0 }

end Point
github
structure Point where
  x : ℤ
  y : ℤ

namespace Point

def origin : Point := { x := 0, y := 0 }

end Point

3. Nested doc comments

a doc comment wrapping an example that has its own comment
horizon-dark
/- computes the successor of a natural number
   /- example: succ 41 = 42 -/
-/
def succ (n : ℕ) : ℕ := n + 1
atom-one-dark
/- computes the successor of a natural number
   /- example: succ 41 = 42 -/
-/
def succ (n : ℕ) : ℕ := n + 1
github-dark
/- computes the successor of a natural number
   /- example: succ 41 = 42 -/
-/
def succ (n : ℕ) : ℕ := n + 1
dracula
/- computes the successor of a natural number
   /- example: succ 41 = 42 -/
-/
def succ (n : ℕ) : ℕ := n + 1
nord
/- computes the successor of a natural number
   /- example: succ 41 = 42 -/
-/
def succ (n : ℕ) : ℕ := n + 1
github
/- computes the successor of a natural number
   /- example: succ 41 = 42 -/
-/
def succ (n : ℕ) : ℕ := n + 1