Blog

Posts

• Hello Verso
  February 14, 2026

  berberman

  • Blog

  It's been 6 years since I first built this site using Hakyll—though I barely posted anything. Recently, I decided to migrate to Verso, a new static site generator written in Lean. It allows me to write posts directly in Lean and seamlessly integrating code snippets:

  theorem Eq.uip {α : Sort u} (x y : α) (h₁ h₂ : x = y) : h₁ = h₂ := byα:Sort ux:αy:αh₁:x = yh₂:x = y⊢ h₁ = h₂ rflAll goals completed! 🐙 Nat.succ (n : Nat) : Nat#check Nat.succ

  Nat.succ (n : Nat) : Nat

  I adapted this site from verso-templates, and with some fine-tuning, I've got Prism.js working for non-Lean languages:

  main :: IO ()
  main = putStrLn "Hello, World!"
  

  Read more