Posts

This blog has been around for a while, but every time I visited it, something about the visual design felt off. The typography was not elegant enough; Lean code blocks had no color scheme; the palette lacked quality; and the font size were not quite right. Overall, the site did not feel modern, and both UI and UX needed work, even though it retained kind of minimalist style. RSS/Atom feeds were also missing.

So I decided to refine the styling on top of existing foundation, and add a few interesting features.

One day my friend CircuitCoder asked 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!

While reading A Few Constructions on Constructors¹, I came across this definition of Heterogeneous Equality (represented here using Lean axioms):

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:

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!"

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—

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.