Archive

Posts

• Dependent Pattern Matching and Convoy Patterns
  April 18, 2026

  berberman

  • Lean

  The other day, I saw my friend CircuitCoder ask a Rocq question in a group chat:

  "How do you prove the following theorem without using the dependent destruction tactic? It seems to require the Convoy Pattern, which I tried learning but still don't quite grasp."

  Inductive vector (A : Type) : nat -> Type :=
    | vnil : vector A 0
    | vcons {n} (v : vector A n) (a : A) : vector A (S n).
  
  Lemma test {A} {n} {v : vector A (S n)} :
    exists v' : vector A n, exists a : A, v = vcons A v' a.
  

  Let's explore dependent pattern matching and the convoy pattern in Lean!

  Read more
• HEq and Axiom K: An Exploration in Lean
  February 23, 2026

  berberman

  • Lean

  While reading Conor McBride's A Few Constructions on Constructors, I came across his definition of Heterogeneous Equality (represented here using Lean axioms):

  Read more
• 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
• Upload Gradle Build Scripts and Android Libraries to GitHub Packages
  July 5, 2023

  berberman

  • Other
  Read more
• Default Language Extensions Enabled in GHCi
  April 11, 2021

  berberman

  • Haskell

  I wrote this post because I stumbled upon the fact that head [] passes type checking in GHCi even with ExtendedDefaultRules disabled. This surprised me. After some investigation—

  Read more
• Setting up a Haskell development environment on Arch Linux
  October 27, 2020

  berberman

  • Haskell

  Once you accept the principles of Arch Linux -- being simplicity and modernity -- everything goes easier. In this article, we will use up-to-date Haskell ecosystem by using system provided Haskell packages, getting rid of awkward stack which could eat huge amount of your disk space. We won't going to nix or ghcup, since they are both general Haskell toolchain solutions, not specific to Arch Linux.

  Read more