dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 11:08:25 +00:00
Code Issues Releases Wiki Activity

Edits

Browse Source
This commit is contained in:
Daniel Hillerström
2021-02-03 22:29:38 +00:00
parent 33781a94e2
commit 756ce77e5a
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
thesis.tex
View File

@@ -7541,7 +7541,7 @@ the parameter $q$.
H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{r_i} \mapsto N_i \}_i H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{r_i} \mapsto N_i \}_i
\el}\\\\ \el}\\\\
\typ{\Delta;\Gamma, q : A', x : A}{M : D}\\\\ \typ{\Delta;\Gamma, q : A', x : A}{M : D}\\\\
[\typ{\Delta;\Gamma,q : A', p_i : A_i, r_i : B_i \to D}{N_i : D}]_i [\typ{\Delta;\Gamma,q : A', p_i : A_i, r_i : \Record{B_i;A'} \to D}{N_i : D}]_i
} }
{\typ{\Delta;\Gamma}{(q^{A'} . H) : \Record{C;A'} \Harrow^\param D}} {\typ{\Delta;\Gamma}{(q^{A'} . H) : \Record{C;A'} \Harrow^\param D}}
\end{mathpar} \end{mathpar}