Add description to expr_pattern

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-11 23:26:07 -07:00
parent 21ab4f0a8b
commit 29a18b8b37

View File

@ -2,6 +2,7 @@
title: "The 'Deeply Embedded Expression' Trick in Agda" title: "The 'Deeply Embedded Expression' Trick in Agda"
date: 2024-03-11T14:25:52-07:00 date: 2024-03-11T14:25:52-07:00
tags: ["Agda"] 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, I've been working on a relatively large Agda project for a few months now,