Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Update "expr pattern in agda" to new math delimiters

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-13 18:50:56 -07:00
parent 6f20b17948
commit b705aa217c
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
content/blog/agda_expr_pattern.md
View File

@ -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