From b705aa217cd4d1a37f02a1285e588d326f32270c Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 13 May 2024 18:50:56 -0700 Subject: [PATCH] Update "expr pattern in agda" to new math delimiters Signed-off-by: Danila Fedorin --- content/blog/agda_expr_pattern.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/content/blog/agda_expr_pattern.md b/content/blog/agda_expr_pattern.md index 3f1ae9b..e1575b6 100644 --- a/content/blog/agda_expr_pattern.md +++ b/content/blog/agda_expr_pattern.md @@ -150,7 +150,7 @@ our expression language, which makes case analysis very difficult. An obvious thing to do with an expression is to evaluate it. This will be important for our proofs, because it will establish a connection between expressions (created via `Expr`) and actual Agda objects that we need to -reason about at the end of the day. The notation \\(\\llbracket e \\rrbracket\\) +reason about at the end of the day. The notation \(\llbracket e \rrbracket\) is commonly used in PL circles for evaluation (it comes from [Denotational Semantics](https://en.wikipedia.org/wiki/Denotational_semantics)). Thus, my Agda evaluation function is written as follows: @@ -188,8 +188,8 @@ the structure of these cases. Thus, examples include: * **Automatic derivation of function properties:** suppose you're interested in working with continuous functions. You also know that the addition, subtraction, and multiplication of two functions preserves continuity. - Of course, the constant function \\(x \\mapsto c\\) and the identity function - \\(x \\mapsto x\\) are continuous too. You may define an expression data type + Of course, the constant function \(x \mapsto c\) and the identity function + \(x \mapsto x\) are continuous too. You may define an expression data type that has cases for these operations. Then, your evaluation function could transform the expression into a plain function, and a proof on the structure of the expression can be used to verify the resulting function's