diff --git a/content/blog/agda_expr_pattern.md b/content/blog/agda_expr_pattern.md index e1575b6..0c6d65d 100644 --- a/content/blog/agda_expr_pattern.md +++ b/content/blog/agda_expr_pattern.md @@ -222,7 +222,7 @@ are the ingredients to this trick: ### Conclusion I'll be the first to admit that this trick is quite situational, and may -not be as far-reaching as the ["Is Something" pattern](https://danilafe.com/blog/agda_is_pattern/) +not be as far-reaching as the ["Is Something" pattern]({{< relref "agda_is_pattern" >}}) I wrote about before, which seems to occur far more in the wild. However, there have now been two times when I personally reached for this trick, which seems to suggest that it may be useful to someone else.