semantic package: Floating premises with nested inference
2
I am typing setting some big step semantics using the package semantic and its command inference.
I use the LuaLaTeX compiler.
However, when I compose more inference commands, and one of them represents an axiom, i.e. a rule without any premises, the other premise starts floating. It looks like it is trying to do some vertical alignment.
Here is an example:
inference[(mathcal{E'}=) textsc{EC-IfF}]
{
% ------- THIS PREMISE FLOATS
overset{mathcal{E'_0}}
{
langle b, σ rangle downarrow texttt{false}
}
&
{
inference
[textsc{EC-Skip}]
{}
{
langle texttt{skip}, σ rangle downarrow σ
}
}
}
{
langle
texttt{if } b texttt{ then }
(c_0 ; texttt{ while } b texttt{ do } c_0)
texttt{ else skip}, σ
rangle
downarrow
σ''
}
luatex overset
edited Mar 8 at 13:30
JouleV
5,97821549
asked Mar 8 at 10:08
EinarEinar
404
add a comment |
2
I am typing setting some big step semantics using the package semantic and its command inference.
I use the LuaLaTeX compiler.
However, when I compose more inference commands, and one of them represents an axiom, i.e. a rule without any premises, the other premise starts floating. It looks like it is trying to do some vertical alignment.
Here is an example:
inference[(mathcal{E'}=) textsc{EC-IfF}]
{
% ------- THIS PREMISE FLOATS
overset{mathcal{E'_0}}
{
langle b, σ rangle downarrow texttt{false}
}
&
{
inference
[textsc{EC-Skip}]
{}
{
langle texttt{skip}, σ rangle downarrow σ
}
}
}
{
langle
texttt{if } b texttt{ then }
(c_0 ; texttt{ while } b texttt{ do } c_0)
texttt{ else skip}, σ
rangle
downarrow
σ''
}
luatex overset
edited Mar 8 at 13:30
JouleV
5,97821549
asked Mar 8 at 10:08
EinarEinar
404
add a comment |
2
2
2
I am typing setting some big step semantics using the package semantic and its command inference.
I use the LuaLaTeX compiler.
However, when I compose more inference commands, and one of them represents an axiom, i.e. a rule without any premises, the other premise starts floating. It looks like it is trying to do some vertical alignment.
Here is an example:
inference[(mathcal{E'}=) textsc{EC-IfF}]
{
% ------- THIS PREMISE FLOATS
overset{mathcal{E'_0}}
{
langle b, σ rangle downarrow texttt{false}
}
&
{
inference
[textsc{EC-Skip}]
{}
{
langle texttt{skip}, σ rangle downarrow σ
}
}
}
{
langle
texttt{if } b texttt{ then }
(c_0 ; texttt{ while } b texttt{ do } c_0)
texttt{ else skip}, σ
rangle
downarrow
σ''
}
luatex overset
edited Mar 8 at 13:30
JouleV
5,97821549
asked Mar 8 at 10:08
EinarEinar
404
I am typing setting some big step semantics using the package semantic and its command inference.
I use the LuaLaTeX compiler.
However, when I compose more inference commands, and one of them represents an axiom, i.e. a rule without any premises, the other premise starts floating. It looks like it is trying to do some vertical alignment.
Here is an example:
inference[(mathcal{E'}=) textsc{EC-IfF}]
{
% ------- THIS PREMISE FLOATS
overset{mathcal{E'_0}}
{
langle b, σ rangle downarrow texttt{false}
}
&
{
inference
[textsc{EC-Skip}]
{}
{
langle texttt{skip}, σ rangle downarrow σ
}
}
}
{
langle
texttt{if } b texttt{ then }
(c_0 ; texttt{ while } b texttt{ do } c_0)
texttt{ else skip}, σ
rangle
downarrow
σ''
}
luatex overset
luatex overset
edited Mar 8 at 13:30
JouleV
5,97821549
asked Mar 8 at 10:08
EinarEinar
404
edited Mar 8 at 13:30
JouleV
5,97821549
asked Mar 8 at 10:08
EinarEinar
404
edited Mar 8 at 13:30
JouleV
5,97821549
edited Mar 8 at 13:30
JouleV
5,97821549
edited Mar 8 at 13:30
JouleV
5,97821549
5,97821549
asked Mar 8 at 10:08
EinarEinar
404
asked Mar 8 at 10:08
EinarEinar
404
asked Mar 8 at 10:08
EinarEinar
404
404
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
2
In the OP's example, the baseline is being preserved across the large "numerator". While one may argue that is the proper way to do it, one can override that default with abovebaseline[-dpstrutbox]{...} applied to the ED-Skip inference.
documentclass{article}
usepackage{semantic,amsmath,stackengine}
begin{document}
inference[(mathcal{E'}=) textsc{EC-IfF}]
{
% ------- THIS PREMISE FLOATS
overset{mathcal{E'_0}}
{
langle b, σ rangle downarrow texttt{false}
}
&
{
abovebaseline[-dpstrutbox]{inference
[textsc{EC-Skip}]
{}
{
langle texttt{skip}, σ rangle downarrow σ
}}
}
}
{
langle
texttt{if } b texttt{ then }
(c_0 ; texttt{ while } b texttt{ do } c_0)
texttt{ else skip}, σ
rangle
downarrow
σ''
}
end{document}
answered Mar 8 at 13:35
Steven B. SegletesSteven B. Segletes
158k9204411
Thank you. The answer works as intended. However, I do not really understand what the problem is «the baseline is being preserved», and why your solution works. Any chance, you could you point me to some reference? Again thank you.
– Einar
yesterday
@Einar Consider the numerator. With theoverset{<over>}{<baseline>}macro, the 2nd term sits on the natural foundation or baseline of the equation, and the 1st term sits above the 2nd. With the next term, theEC-Skipalso sits on this same baseline. They are thus at the same vertical height in your example. The fraction-like-thing that follows is set up so that the horizontal line goes through the central math axis (i.e., centered at the same height as a minus sign above the baseline), with the<skip,>downarrowtext being set below this axis line.
– Steven B. Segletes
yesterday
@Einar In summary, while you can force things to go up and down, there is a natural vertical location that things want to sit at. And the way your "numerator" was composed, the<b,>downarrow falsewants to sit at the same vertical height asEC-Skip.
– Steven B. Segletes
yesterday
@Einar The macroabovebaselinesays to force the argument (the whole object taken as a box) to sit on a line the optionally specified distance above the natural baseline. By providing it a negative distance, it says to sit on a specified line below the natural baseline. The value of-dpstrutboxis the length equal to the natural depth of a text line. So I told it to set that 2nd term of the numerator so that it sits on a line located at the natural depth of a simple line of text.
– Steven B. Segletes
yesterday
add a comment |
Your Answer
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "85"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: false,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: null,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
draft saved
draft discarded
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2ftex.stackexchange.com%2fquestions%2f478383%2fsemantic-package-floating-premises-with-nested-inference%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
2
In the OP's example, the baseline is being preserved across the large "numerator". While one may argue that is the proper way to do it, one can override that default with abovebaseline[-dpstrutbox]{...} applied to the ED-Skip inference.
documentclass{article}
usepackage{semantic,amsmath,stackengine}
begin{document}
inference[(mathcal{E'}=) textsc{EC-IfF}]
{
% ------- THIS PREMISE FLOATS
overset{mathcal{E'_0}}
{
langle b, σ rangle downarrow texttt{false}
}
&
{
abovebaseline[-dpstrutbox]{inference
[textsc{EC-Skip}]
{}
{
langle texttt{skip}, σ rangle downarrow σ
}}
}
}
{
langle
texttt{if } b texttt{ then }
(c_0 ; texttt{ while } b texttt{ do } c_0)
texttt{ else skip}, σ
rangle
downarrow
σ''
}
end{document}
answered Mar 8 at 13:35
Steven B. SegletesSteven B. Segletes
158k9204411
Thank you. The answer works as intended. However, I do not really understand what the problem is «the baseline is being preserved», and why your solution works. Any chance, you could you point me to some reference? Again thank you.
– Einar
yesterday
@Einar Consider the numerator. With theoverset{<over>}{<baseline>}macro, the 2nd term sits on the natural foundation or baseline of the equation, and the 1st term sits above the 2nd. With the next term, theEC-Skipalso sits on this same baseline. They are thus at the same vertical height in your example. The fraction-like-thing that follows is set up so that the horizontal line goes through the central math axis (i.e., centered at the same height as a minus sign above the baseline), with the<skip,>downarrowtext being set below this axis line.
– Steven B. Segletes
yesterday
@Einar In summary, while you can force things to go up and down, there is a natural vertical location that things want to sit at. And the way your "numerator" was composed, the<b,>downarrow falsewants to sit at the same vertical height asEC-Skip.
– Steven B. Segletes
yesterday
@Einar The macroabovebaselinesays to force the argument (the whole object taken as a box) to sit on a line the optionally specified distance above the natural baseline. By providing it a negative distance, it says to sit on a specified line below the natural baseline. The value of-dpstrutboxis the length equal to the natural depth of a text line. So I told it to set that 2nd term of the numerator so that it sits on a line located at the natural depth of a simple line of text.
– Steven B. Segletes
yesterday
add a comment |
2
In the OP's example, the baseline is being preserved across the large "numerator". While one may argue that is the proper way to do it, one can override that default with abovebaseline[-dpstrutbox]{...} applied to the ED-Skip inference.
documentclass{article}
usepackage{semantic,amsmath,stackengine}
begin{document}
inference[(mathcal{E'}=) textsc{EC-IfF}]
{
% ------- THIS PREMISE FLOATS
overset{mathcal{E'_0}}
{
langle b, σ rangle downarrow texttt{false}
}
&
{
abovebaseline[-dpstrutbox]{inference
[textsc{EC-Skip}]
{}
{
langle texttt{skip}, σ rangle downarrow σ
}}
}
}
{
langle
texttt{if } b texttt{ then }
(c_0 ; texttt{ while } b texttt{ do } c_0)
texttt{ else skip}, σ
rangle
downarrow
σ''
}
end{document}
answered Mar 8 at 13:35
Steven B. SegletesSteven B. Segletes
158k9204411
Thank you. The answer works as intended. However, I do not really understand what the problem is «the baseline is being preserved», and why your solution works. Any chance, you could you point me to some reference? Again thank you.
– Einar
yesterday
@Einar Consider the numerator. With theoverset{<over>}{<baseline>}macro, the 2nd term sits on the natural foundation or baseline of the equation, and the 1st term sits above the 2nd. With the next term, theEC-Skipalso sits on this same baseline. They are thus at the same vertical height in your example. The fraction-like-thing that follows is set up so that the horizontal line goes through the central math axis (i.e., centered at the same height as a minus sign above the baseline), with the<skip,>downarrowtext being set below this axis line.
– Steven B. Segletes
yesterday
@Einar In summary, while you can force things to go up and down, there is a natural vertical location that things want to sit at. And the way your "numerator" was composed, the<b,>downarrow falsewants to sit at the same vertical height asEC-Skip.
– Steven B. Segletes
yesterday
@Einar The macroabovebaselinesays to force the argument (the whole object taken as a box) to sit on a line the optionally specified distance above the natural baseline. By providing it a negative distance, it says to sit on a specified line below the natural baseline. The value of-dpstrutboxis the length equal to the natural depth of a text line. So I told it to set that 2nd term of the numerator so that it sits on a line located at the natural depth of a simple line of text.
– Steven B. Segletes
yesterday
add a comment |
2
2
2
In the OP's example, the baseline is being preserved across the large "numerator". While one may argue that is the proper way to do it, one can override that default with abovebaseline[-dpstrutbox]{...} applied to the ED-Skip inference.
documentclass{article}
usepackage{semantic,amsmath,stackengine}
begin{document}
inference[(mathcal{E'}=) textsc{EC-IfF}]
{
% ------- THIS PREMISE FLOATS
overset{mathcal{E'_0}}
{
langle b, σ rangle downarrow texttt{false}
}
&
{
abovebaseline[-dpstrutbox]{inference
[textsc{EC-Skip}]
{}
{
langle texttt{skip}, σ rangle downarrow σ
}}
}
}
{
langle
texttt{if } b texttt{ then }
(c_0 ; texttt{ while } b texttt{ do } c_0)
texttt{ else skip}, σ
rangle
downarrow
σ''
}
end{document}
answered Mar 8 at 13:35
Steven B. SegletesSteven B. Segletes
158k9204411
In the OP's example, the baseline is being preserved across the large "numerator". While one may argue that is the proper way to do it, one can override that default with abovebaseline[-dpstrutbox]{...} applied to the ED-Skip inference.
documentclass{article}
usepackage{semantic,amsmath,stackengine}
begin{document}
inference[(mathcal{E'}=) textsc{EC-IfF}]
{
% ------- THIS PREMISE FLOATS
overset{mathcal{E'_0}}
{
langle b, σ rangle downarrow texttt{false}
}
&
{
abovebaseline[-dpstrutbox]{inference
[textsc{EC-Skip}]
{}
{
langle texttt{skip}, σ rangle downarrow σ
}}
}
}
{
langle
texttt{if } b texttt{ then }
(c_0 ; texttt{ while } b texttt{ do } c_0)
texttt{ else skip}, σ
rangle
downarrow
σ''
}
end{document}
answered Mar 8 at 13:35
Steven B. SegletesSteven B. Segletes
158k9204411
answered Mar 8 at 13:35
Steven B. SegletesSteven B. Segletes
158k9204411
answered Mar 8 at 13:35
Steven B. SegletesSteven B. Segletes
158k9204411
answered Mar 8 at 13:35
Steven B. SegletesSteven B. Segletes
158k9204411
158k9204411
Thank you. The answer works as intended. However, I do not really understand what the problem is «the baseline is being preserved», and why your solution works. Any chance, you could you point me to some reference? Again thank you.
– Einar
yesterday
@Einar Consider the numerator. With theoverset{<over>}{<baseline>}macro, the 2nd term sits on the natural foundation or baseline of the equation, and the 1st term sits above the 2nd. With the next term, theEC-Skipalso sits on this same baseline. They are thus at the same vertical height in your example. The fraction-like-thing that follows is set up so that the horizontal line goes through the central math axis (i.e., centered at the same height as a minus sign above the baseline), with the<skip,>downarrowtext being set below this axis line.
– Steven B. Segletes
yesterday
@Einar In summary, while you can force things to go up and down, there is a natural vertical location that things want to sit at. And the way your "numerator" was composed, the<b,>downarrow falsewants to sit at the same vertical height asEC-Skip.
– Steven B. Segletes
yesterday
@Einar The macroabovebaselinesays to force the argument (the whole object taken as a box) to sit on a line the optionally specified distance above the natural baseline. By providing it a negative distance, it says to sit on a specified line below the natural baseline. The value of-dpstrutboxis the length equal to the natural depth of a text line. So I told it to set that 2nd term of the numerator so that it sits on a line located at the natural depth of a simple line of text.
– Steven B. Segletes
yesterday
add a comment |
Thank you. The answer works as intended. However, I do not really understand what the problem is «the baseline is being preserved», and why your solution works. Any chance, you could you point me to some reference? Again thank you.
– Einar
yesterday
@Einar Consider the numerator. With theoverset{<over>}{<baseline>}macro, the 2nd term sits on the natural foundation or baseline of the equation, and the 1st term sits above the 2nd. With the next term, theEC-Skipalso sits on this same baseline. They are thus at the same vertical height in your example. The fraction-like-thing that follows is set up so that the horizontal line goes through the central math axis (i.e., centered at the same height as a minus sign above the baseline), with the<skip,>downarrowtext being set below this axis line.
– Steven B. Segletes
yesterday
@Einar In summary, while you can force things to go up and down, there is a natural vertical location that things want to sit at. And the way your "numerator" was composed, the<b,>downarrow falsewants to sit at the same vertical height asEC-Skip.
– Steven B. Segletes
yesterday
@Einar The macroabovebaselinesays to force the argument (the whole object taken as a box) to sit on a line the optionally specified distance above the natural baseline. By providing it a negative distance, it says to sit on a specified line below the natural baseline. The value of-dpstrutboxis the length equal to the natural depth of a text line. So I told it to set that 2nd term of the numerator so that it sits on a line located at the natural depth of a simple line of text.
– Steven B. Segletes
yesterday
Thank you. The answer works as intended. However, I do not really understand what the problem is «the baseline is being preserved», and why your solution works. Any chance, you could you point me to some reference? Again thank you.
– Einar
yesterday
Thank you. The answer works as intended. However, I do not really understand what the problem is «the baseline is being preserved», and why your solution works. Any chance, you could you point me to some reference? Again thank you.
– Einar
yesterday
@Einar Consider the numerator. With the
overset{<over>}{<baseline>} macro, the 2nd term sits on the natural foundation or baseline of the equation, and the 1st term sits above the 2nd. With the next term, the EC-Skip also sits on this same baseline. They are thus at the same vertical height in your example. The fraction-like-thing that follows is set up so that the horizontal line goes through the central math axis (i.e., centered at the same height as a minus sign above the baseline), with the <skip,>downarrow text being set below this axis line.– Steven B. Segletes
yesterday
@Einar Consider the numerator. With the
overset{<over>}{<baseline>} macro, the 2nd term sits on the natural foundation or baseline of the equation, and the 1st term sits above the 2nd. With the next term, the EC-Skip also sits on this same baseline. They are thus at the same vertical height in your example. The fraction-like-thing that follows is set up so that the horizontal line goes through the central math axis (i.e., centered at the same height as a minus sign above the baseline), with the <skip,>downarrow text being set below this axis line.– Steven B. Segletes
yesterday
@Einar In summary, while you can force things to go up and down, there is a natural vertical location that things want to sit at. And the way your "numerator" was composed, the
<b,>downarrow false wants to sit at the same vertical height as EC-Skip.– Steven B. Segletes
yesterday
@Einar In summary, while you can force things to go up and down, there is a natural vertical location that things want to sit at. And the way your "numerator" was composed, the
<b,>downarrow false wants to sit at the same vertical height as EC-Skip.– Steven B. Segletes
yesterday
@Einar The macro
abovebaseline says to force the argument (the whole object taken as a box) to sit on a line the optionally specified distance above the natural baseline. By providing it a negative distance, it says to sit on a specified line below the natural baseline. The value of -dpstrutbox is the length equal to the natural depth of a text line. So I told it to set that 2nd term of the numerator so that it sits on a line located at the natural depth of a simple line of text.– Steven B. Segletes
yesterday
@Einar The macro
abovebaseline says to force the argument (the whole object taken as a box) to sit on a line the optionally specified distance above the natural baseline. By providing it a negative distance, it says to sit on a specified line below the natural baseline. The value of -dpstrutbox is the length equal to the natural depth of a text line. So I told it to set that 2nd term of the numerator so that it sits on a line located at the natural depth of a simple line of text.– Steven B. Segletes
yesterday
add a comment |
draft saved
draft discarded
Thanks for contributing an answer to TeX - LaTeX Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
draft saved
draft discarded
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2ftex.stackexchange.com%2fquestions%2f478383%2fsemantic-package-floating-premises-with-nested-inference%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
