mirror of
https://github.com/thufschmitt/tix-papers.git
synced 2024-08-16 16:20:47 +03:00
parent
eb5abd20f1
commit
4ecb8f3711
@ -84,6 +84,7 @@
|
||||
\newcommand{\Γ}{\Gamma}
|
||||
\newcommand{\τ}{\tau}
|
||||
\newcommand{\σ}{\sigma}
|
||||
\newcommand{\λ}{\lambda}
|
||||
\newcommand{\recleq}{\sqsubsetleq}
|
||||
\newcommand{\discrete}[2]{\left\{ #1, \ldots{}, #2 \right\}}
|
||||
|
||||
|
@ -3,7 +3,7 @@
|
||||
<e> ::=
|
||||
\x/ \| \c/
|
||||
\alt \e/.\a/ \| \e/.\a/ or \e/
|
||||
\alt \p/:\e/ \| \e/ \e/
|
||||
\alt $\λ$\p/.\e/ \| \e/ \e/
|
||||
\alt \{ \e/ = \e/ \}
|
||||
\alt with \e/; \e/
|
||||
\alt (\x/ := \e/ $\bm{\in}$ \t/) ? \e/ : \e/
|
||||
|
@ -3,7 +3,7 @@
|
||||
|
||||
<v> ::=
|
||||
\c/
|
||||
\alt \p/:\e/
|
||||
\alt $\λ$\p/.\e/
|
||||
\alt \{ \v/ = \e/ \} $\orthplus \cdots{} \orthplus$ \{ \v/ = \e/ \}
|
||||
\alt Cons(\e/, \e/) \| nil
|
||||
\end{grammar}
|
||||
|
@ -10,8 +10,8 @@ figure~\pref{fig:semantics:nix-light:patterns}
|
||||
\dstepa{\{ \s/ = \e/; $\ldots{}$\}.\s/}{$e$}{}
|
||||
\dstepa{\{ \s/ = \e/; $\ldots{}$\}.\s/ or $e'$}{$e$}{}
|
||||
\dstepa{$v.s \text{ or } e'$}{$e'$}{if $\v/ \neq$ \{ \s/ = \e/; $\ldots{}$ \}}
|
||||
\dstepa{$(x:e_1) e_2$}{$\substp{x}{e_2}{e_1}$}{}
|
||||
\dstepa{$(p:e_1) v$} {$\substp{p}{v}{e_1}$}{if $p \neq x$}
|
||||
\dstepa{$(\λ x.e_1) e_2$}{$\substp{x}{e_2}{e_1}$}{}
|
||||
\dstepa{$(\λ p.e_1) v$} {$\substp{p}{v}{e_1}$}{if $p \neq x$}
|
||||
\dstepa{with \{ $l_1$ = $e_1$; $\cdots{}$; $l_n$ = $e_n$; \} ; \e/}{
|
||||
\e/[\assign{l_1}{\eone}; ...; \assign{l_n}{\en}]
|
||||
}{}
|
||||
|
Loading…
Reference in New Issue
Block a user