pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Typo in translation rule

Browse source
This commit is contained in:
Adam Chlipala 2020-04-15 09:48:24 -04:00
parent d74a0ebb42
commit c607913898
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
frap_book.tex
View file

@ -4079,7 +4079,7 @@ We will define a judgment $\dscomp{v}{c}{s}$, indicating that mixed-embedded com
A good warmup is defining a related judgment $\dscomp{v}{n}{e}$, compiling normal Gallina numeric expressions $n$ into syntactic expressions $e$. A good warmup is defining a related judgment $\dscomp{v}{n}{e}$, compiling normal Gallina numeric expressions $n$ into syntactic expressions $e$.
$$\infer{\dscomp{v}{x}{n}}{ $$\infer{\dscomp{v}{n}{x}}{
v(x) = n v(x) = n
} }
\quad \infer{\dscomp{v}{n_1 + n_2}{e_1 + e_2}}{ \quad \infer{\dscomp{v}{n_1 + n_2}{e_1 + e_2}}{