Posts
-
Dependent Pattern Matching and Convoy Patterns
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 destructiontactic? 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
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
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₂ := α:Sort ux:αy:αh₁:x = yh₂:x = y⊢ h₁ = h₂ All goals completed! 🐙#check Nat.succI adapted this site from verso-templates, and with some fine-tuning, I've got Prism.js working for non-Lean languages:
Read moremain :: IO () main = putStrLn "Hello, World!" - Upload Gradle Build Scripts and Android Libraries to GitHub Packages Read more
-
Default Language Extensions Enabled in GHCi
I wrote this post because I stumbled upon the fact that
Read morehead []passes type checking in GHCi even withExtendedDefaultRulesdisabled. This surprised me. After some investigation— -
Setting up a Haskell development environment on Arch Linux
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