From 29a18b8b371313fe5a312ae0a0ecedc2594b1b01 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 11 Mar 2024 23:26:07 -0700 Subject: [PATCH] Add description to expr_pattern Signed-off-by: Danila Fedorin --- content/blog/agda_expr_pattern.md | 1 + 1 file changed, 1 insertion(+) 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,