equal
deleted
inserted
replaced
1230 binding clauses, except for empty binding clauses are defined as follows: |
1230 binding clauses, except for empty binding clauses are defined as follows: |
1231 % |
1231 % |
1232 \begin{equation}\label{bnemptybinder} |
1232 \begin{equation}\label{bnemptybinder} |
1233 \mbox{% |
1233 \mbox{% |
1234 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1234 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1235 \multicolumn{2}{@ {}l}{\isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ |
1235 \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ |
1236 $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} does not occur in @{text "rhs"} |
1236 $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} does not occur in @{text "rhs"} |
1237 and the free-variable function for the type of @{text "y"} is @{text "fv_ty"}\\ |
1237 and the free-variable function for the type of @{text "y"} is @{text "fv_ty"}\\ |
1238 $\bullet$ & @{term "v = fv_bn y"} provided @{text "y"} occurs in @{text "rhs"} |
1238 $\bullet$ & @{term "v = fv_bn y"} provided @{text "y"} occurs in @{text "rhs"} |
1239 with a recursive call @{text "bn y"}\\ |
1239 with a recursive call @{text "bn y"}\\ |
1240 $\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in @{text "rhs"}, |
1240 $\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in @{text "rhs"}, |