diff --git a/content/blog/agda_expr_pattern.md b/content/blog/agda_expr_pattern.md index 2250f0e..28b7650 100644 --- a/content/blog/agda_expr_pattern.md +++ b/content/blog/agda_expr_pattern.md @@ -2,6 +2,7 @@ title: "The 'Deeply Embedded Expression' Trick in Agda" date: 2024-03-11T14:25:52-07:00 tags: ["Agda"] +description: "In this post, I talk about a trick I developed to simplify certain Agda proofs." --- I've been working on a relatively large Agda project for a few months now,