lab14: format stuff
This commit is contained in:
File diff suppressed because it is too large
Load Diff
@@ -26,6 +26,8 @@ First, write the evaluation order rules (using small-step semantics) for the exp
|
|||||||
Next, define the typing rules for these expressions. Be sure that your typing rules guarantee both progress and preservation. (For ways of formally guaranteeing these properties, see Chapter 8 of Ben Pierce's "Types and Programming Languages").
|
Next, define the typing rules for these expressions. Be sure that your typing rules guarantee both progress and preservation. (For ways of formally guaranteeing these properties, see Chapter 8 of Ben Pierce's "Types and Programming Languages").
|
||||||
*/
|
*/
|
||||||
|
|
||||||
|
#set page(columns: 2)
|
||||||
|
|
||||||
// Language keywords rendered in monospace
|
// Language keywords rendered in monospace
|
||||||
#let kw(body) = text(font: "DejaVu Sans Mono", size: 0.85em, body)
|
#let kw(body) = text(font: "DejaVu Sans Mono", size: 0.85em, body)
|
||||||
|
|
||||||
@@ -56,23 +58,20 @@ Next, define the typing rules for these expressions. Be sure that your typing ru
|
|||||||
// Rule: fraction with name on the left
|
// Rule: fraction with name on the left
|
||||||
// premises (content), conclusion (content)
|
// premises (content), conclusion (content)
|
||||||
#let rule(name, premises, conclusion) = {
|
#let rule(name, premises, conclusion) = {
|
||||||
grid(
|
stack(
|
||||||
columns: (auto, auto),
|
dir: ttb,
|
||||||
column-gutter: 1em,
|
spacing: 0.4em,
|
||||||
align: (right + horizon, left + horizon),
|
|
||||||
rel(name),
|
rel(name),
|
||||||
box(stroke: 0.5pt, inset: 4pt, math.equation(
|
box(stroke: 0.5pt, inset: 4pt, math.equation(
|
||||||
block: true,
|
block: true,
|
||||||
numbering: none,
|
numbering: none,
|
||||||
// if premises != "" {
|
|
||||||
math.frac(premises, conclusion),
|
math.frac(premises, conclusion),
|
||||||
// } else { conclusion },
|
|
||||||
)),
|
)),
|
||||||
)
|
)
|
||||||
v(0.4em)
|
v(0.8em)
|
||||||
}
|
}
|
||||||
|
|
||||||
== Operational Semantics Rules
|
= Evaluation Rules
|
||||||
|
|
||||||
#v(0.6em)
|
#v(0.6em)
|
||||||
|
|
||||||
@@ -102,7 +101,8 @@ Next, define the typing rules for these expressions. Be sure that your typing ru
|
|||||||
#rule("E-StrLen-Zero", "", $#sstep[#strlen[`""`]][0]$)
|
#rule("E-StrLen-Zero", "", $#sstep[#strlen[`""`]][0]$)
|
||||||
#rule("E-StrLen-NonZero", [c is a single char, $s = c + s'$], $#sstep[#strlen[$s$]][#suc[#strlen[$s'$]]]$)
|
#rule("E-StrLen-NonZero", [c is a single char, $s = c + s'$], $#sstep[#strlen[$s$]][#suc[#strlen[$s'$]]]$)
|
||||||
|
|
||||||
== Typing Rules
|
#pagebreak()
|
||||||
|
= Typing Rules
|
||||||
|
|
||||||
#v(0.6em)
|
#v(0.6em)
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user