Skip to content

Commit

Permalink
ammend stepper doc to new spec (#1649)
Browse files Browse the repository at this point in the history
Co-authored-by: Martin Henz <[email protected]>
  • Loading branch information
hanscau and martin-henz authored Apr 8, 2024
1 parent 1692d26 commit 37329c2
Showing 1 changed file with 4 additions and 20 deletions.
24 changes: 4 additions & 20 deletions docs/specs/source_2_stepper_rules.tex
Original file line number Diff line number Diff line change
Expand Up @@ -369,7 +369,6 @@ \subsection*{Expresssions: Blocks}
\sEntry{Block-expression-return-reduce-1}{In a block expression starting with
a value statement and then a return statement, the value statement can be
removed.}

\gentzen{}{
\sCode{
\{\sVar{value};
Expand All @@ -382,28 +381,13 @@ \subsection*{Expresssions: Blocks}
}
}

\sEntry{Block-expression-return-reduce-2}{A return statement as the first
statement in a block expression can be reduced by reducing the return
expression.}
\gentzen{
\sVar{return-expression}
\ \Rightarrow \
\sVar{return-expression}'
}{
\sKw{\{} \sKw{return } \sVar{return-expression} \sKw{; }
\sVar{statement\ldots} \sKw{\}}
\Rightarrow
\sKw{\{} \sKw{return } \sVar{return-expression}' \sKw{; }
\sVar{statement\ldots} \sKw{\}}
}

\sEntry{Block-expression-return-reduce-3}{A block expression starting with a
return statement reduces to the value of the return statement.}
\sEntry{Block-expression-return-reduce-2}{A block expression starting with a
return statement reduces to the expression of the return statement.}
\gentzen{}{
\sKw{\{} \sKw{return } \sVar{value} \sKw{; }
\sKw{\{} \sKw{return } \sVar{return-expression} \sKw{; }
\sVar{statement\ldots} \sKw{\}}
\Rightarrow
\sVar{value}
\sVar{return-expression}
}

Block expressions are currently used only as expanded forms of functions.
Expand Down

0 comments on commit 37329c2

Please sign in to comment.