From da01f156c51c5a5b7b85040fbfccd492c5036e8a Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Thu, 20 Aug 2020 21:09:58 +0000 Subject: ebproof (20aug20) git-svn-id: svn://tug.org/texlive/trunk@56139 c570f23f-e606-0410-a88d-b1316a301751 --- Master/texmf-dist/tex/latex/ebproof/ebproof.sty | 899 +++++++++--------------- 1 file changed, 331 insertions(+), 568 deletions(-) (limited to 'Master/texmf-dist/tex/latex/ebproof') diff --git a/Master/texmf-dist/tex/latex/ebproof/ebproof.sty b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty index 7601f8e9e85..c2d1d0812e7 100644 --- a/Master/texmf-dist/tex/latex/ebproof/ebproof.sty +++ b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty @@ -1,117 +1,86 @@ -% The ebproof package - Formal proofs in the style of sequent calculus - -%% ebproof.sty -%% Copyright 2017 Emmanuel Beffara - -% This work may be distributed and/or modified under the -% conditions of the LaTeX Project Public License, either version 1.3 -% of this license or (at your option) any later version. -% The latest version of this license is in -% http://www.latex-project.org/lppl.txt -% and version 1.3 or later is part of all distributions of LaTeX -% version 2005/12/01 or later. - -% This work has the LPPL maintenance status `maintained'. - -% The Current Maintainer of this work is Emmanuel Beffara. - -% This work consists of the files ebproof.sty and ebproof.tex. - +%% +%% This is file `ebproof.sty', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% ebproof.dtx (with options: `package') +%% +%% IMPORTANT NOTICE: +%% +%% For the copyright see the source file. +%% +%% Any modified versions of this file must be renamed +%% with new filenames distinct from ebproof.sty. +%% +%% For distribution of the original source see the terms +%% for copying and modification in the file ebproof.dtx. +%% +%% This generated file may be distributed as long as the +%% original source files, as listed above, are part of the +%% same distribution. (The sources need not necessarily be +%% in the same archive or directory.) \NeedsTeXFormat{LaTeX2e} \RequirePackage{expl3} \RequirePackage{xparse} -\ProvidesExplPackage{ebproof}{2017/05/17}{2.0}{EB's proof trees} - - -%% Parameters - -%%% Declaration of the parameters - +\ProvidesExplPackage{ebproof}{2020/08/19}{2.1}{EB's proof trees} \keys_define:nn { ebproof } { - -% general shape - -center .bool_set:N = \l_ebproof_center_bool, - +center .bool_set:N = \l__ebproof_center_bool, proof~style .choice: , -proof~style / upwards .code:n = \bool_set_false:N \l_ebproof_updown_bool, -proof~style / downwards .code:n = \bool_set_true:N \l_ebproof_updown_bool, - -% spacing - -separation .dim_set:N = \l_ebproof_separation_dim, -rule~margin .dim_set:N = \l_ebproof_rule_margin_dim, - -% shape of inference lines - -rule~thickness .dim_set:N = \l_ebproof_rule_thickness_dim, -rule~separation .dim_set:N = \l_ebproof_rule_separation_dim, -rule~dash~length .dim_set:N = \l_ebproof_rule_dash_length_dim, -rule~dash~space .dim_set:N = \l_ebproof_rule_dash_space_dim, -rule~code .tl_set:N = \l_ebproof_rule_code_tl, - +proof~style / upwards .code:n = \bool_set_false:N \l__ebproof_updown_bool, +proof~style / downwards .code:n = \bool_set_true:N \l__ebproof_updown_bool, +separation .dim_set:N = \l__ebproof_separation_dim, +rule~margin .dim_set:N = \l__ebproof_rule_margin_dim, +rule~thickness .dim_set:N = \l__ebproof_rule_thickness_dim, +rule~separation .dim_set:N = \l__ebproof_rule_separation_dim, +rule~dash~length .dim_set:N = \l__ebproof_rule_dash_length_dim, +rule~dash~space .dim_set:N = \l__ebproof_rule_dash_space_dim, +rule~code .tl_set:N = \l__ebproof_rule_code_tl, rule~style .choice:, - -% templates - -template .tl_set:N = \l_ebproof_template_tl, -left~template .tl_set:N = \l_ebproof_left_template_tl, -right~template .tl_set:N = \l_ebproof_right_template_tl, - -% labels - -left~label .tl_set:N = \l_ebproof_left_label_tl, -right~label .tl_set:N = \l_ebproof_right_label_tl, -left~label~template .tl_set:N = \l_ebproof_left_label_template_tl, -right~label~template .tl_set:N = \l_ebproof_right_label_template_tl, -label~separation .dim_set:N = \l_ebproof_label_separation_dim, -label~axis .dim_set:N = \l_ebproof_label_axis_dim, - -} - -%%% Rule styles - +template .tl_set:N = \l__ebproof_template_tl, +left~template .tl_set:N = \l__ebproof_left_template_tl, +right~template .tl_set:N = \l__ebproof_right_template_tl, +left~label .tl_set:N = \l__ebproof_left_label_tl, +right~label .tl_set:N = \l__ebproof_right_label_tl, +left~label~template .tl_set:N = \l__ebproof_left_label_template_tl, +right~label~template .tl_set:N = \l__ebproof_right_label_template_tl, +label~separation .dim_set:N = \l__ebproof_label_separation_dim, +label~axis .dim_set:N = \l__ebproof_label_axis_dim, +} \NewDocumentCommand \ebproofnewrulestyle { mm } { \keys_define:nn { ebproof } { rule~style / #1 .meta:nn = { ebproof } { #2 } } } - \ebproofnewrulestyle { simple } { - rule~code = { \tex_hrule:D height \l_ebproof_rule_thickness_dim } + rule~code = { \tex_hrule:D height \l__ebproof_rule_thickness_dim } } - \ebproofnewrulestyle { no~rule } { rule~code = } - \ebproofnewrulestyle { double } { rule~code = { - \tex_hrule:D height \l_ebproof_rule_thickness_dim - \skip_vertical:N \l_ebproof_rule_separation_dim - \tex_hrule:D height \l_ebproof_rule_thickness_dim + \tex_hrule:D height \l__ebproof_rule_thickness_dim + \skip_vertical:N \l__ebproof_rule_separation_dim + \tex_hrule:D height \l__ebproof_rule_thickness_dim } } - \ebproofnewrulestyle { dashed } { rule~code = { \hbox_to_wd:nn { \tex_hsize:D } { - \dim_set:Nn \l_tmpa_dim { \l_ebproof_rule_dash_space_dim / 2 } + \dim_set:Nn \l_tmpa_dim { \l__ebproof_rule_dash_space_dim / 2 } \skip_horizontal:n { -\l_tmpa_dim } \tex_cleaders:D \hbox:n { \skip_horizontal:N \l_tmpa_dim \tex_vrule:D - height \l_ebproof_rule_thickness_dim - width \l_ebproof_rule_dash_length_dim + height \l__ebproof_rule_thickness_dim + width \l__ebproof_rule_dash_length_dim \skip_horizontal:N \l_tmpa_dim - }\tex_hfill:D + } \tex_hfill:D \skip_horizontal:n { -\l_tmpa_dim } } } } - -%%% Default values - \keys_set:nn { ebproof } { center = true, proof~style = upwards, @@ -132,513 +101,321 @@ label~axis .dim_set:N = \l_ebproof_label_axis_dim, label~separation = 0.5em, label~axis = 0.5ex } - -%%% Defining style macros - \NewDocumentCommand \ebproofnewstyle { mm } { \keys_define:nn { ebproof } { #1 .meta:n = { #2 } } } - - -%% Proof trees - -% Proof trees are represented as a data structure that consists of a box and a -% set of marks, which are vertical positions in the box (as distances from the -% left edge). Arbitrary marks can be defined, the folowing are used for -% alignment: -% - left : the left of the conclusion -% - right : the right of the conclusion -% - axis : the vertical axis of the conclusion - - -%%% Registers - -% TeX does not actually provide data structures, so we have to encode things. -% We provide an allocator for "registers" holding boxes with attributes. Such -% a register consists in a box register and a property list for marks, which -% maps mark names to values as explicit dimensions with units. - -% Create a new register. - -\cs_new:Nn \ebproof_new:N { - \box_new:N #1 - \prop_new:c { l_ebproof_marks_ \__int_value:w #1 _prop } -} - -% Clear a register. - -\cs_new:Nn \ebproof_clear:N { - \hbox_set:Nn #1 {} - % Using \box_clear:N instead would not work because trying to push this box - % on the stack would not actually append any box. - \prop_clear:c { l_ebproof_marks_ \__int_value:w #1 _prop } - \ebproof_set_mark:Nnn #1 { left } { 0pt } - \ebproof_set_mark:Nnn #1 { right } { 0pt } - \ebproof_set_mark:Nnn #1 { axis } { 0pt } -} - - -%%% Mark operations - -% Set the value of a mark. The third argument is a dimension expression. - -\dim_new:N \l_ebproof_transit_dim - -\cs_new:Nn \ebproof_set_mark:Nnn { - \dim_set:Nn \l_ebproof_transit_dim { #3 } - \prop_put:cnV { l_ebproof_marks_ \__int_value:w #1 _prop } { #2 } - \l_ebproof_transit_dim -} - -% Get the value of a mark. This is expandable and can be used in expressions. - -\cs_new:Nn \ebproof_mark:Nn { - \prop_item:cn { l_ebproof_marks_ \__int_value:w #1 _prop } { #2 } -} - -% Shift the marks by a specified amount, without modifying the box. - -\cs_new:Nn \ebproof_shift_x:Nn { - \prop_map_inline:cn { l_ebproof_marks_ \__int_value:w #1 _prop } { - \ebproof_set_mark:Nnn #1 { ##1 } { ##2 + #2 } +\int_new:N \g__ebproof_register_int +\cs_new:Nn \__ebproof_box:N { g__ebproof_box_ \tl_use:N #1 } +\cs_new:Nn \__ebproof_marks:N { g__ebproof_marks_ \tl_use:N #1 } +\cs_new:Nn \__ebproof_new:N { + \tl_new:N #1 + \int_gincr:N \g__ebproof_register_int + \tl_gset:Nx #1 { \int_to_arabic:n { \g__ebproof_register_int } } + \box_new:c { \__ebproof_box:N #1 } + \prop_new:c { \__ebproof_marks:N #1 } +} +\cs_new:Nn \__ebproof_clear:N { + \hbox_set:cn { \__ebproof_box:N #1 } {} + \prop_clear:c { \__ebproof_marks:N #1 } + \__ebproof_set_mark:Nnn #1 { left } { 0pt } + \__ebproof_set_mark:Nnn #1 { right } { 0pt } + \__ebproof_set_mark:Nnn #1 { axis } { 0pt } +} +\dim_new:N \l__ebproof_transit_dim +\cs_new:Nn \__ebproof_set_mark:Nnn { + \dim_set:Nn \l__ebproof_transit_dim { #3 } + \prop_put:cnV { \__ebproof_marks:N #1 } { #2 } + \l__ebproof_transit_dim +} +\cs_new:Nn \__ebproof_mark:Nn { + \prop_item:cn { \__ebproof_marks:N #1 } { #2 } +} +\cs_new:Nn \__ebproof_shift_x:Nn { + \prop_map_inline:cn { \__ebproof_marks:N #1 } { + \__ebproof_set_mark:Nnn #1 { ##1 } { ##2 + #2 } } } - -% Move the left and right marks of the first tree so that they are at least as -% far from the axis as they are in the second tree. For instance if the marks -% are set as -% 1: L---A-------R -% 2: L-------A---R -% then the marks of the first tree are then set as -% 1: L-------A-------R -% The contents of the tree are unchanged. - -\cs_new:Nn \ebproof_enlarge_conclusion:NN { - \dim_set:Nn \l_tmpa_dim { \ebproof_mark:Nn #1 {axis} - + \ebproof_mark:Nn #2 {left} - \ebproof_mark:Nn #2 {axis} } - \dim_compare:nNnT { \l_tmpa_dim } < { \ebproof_mark:Nn #1 {left} } { - \ebproof_set_mark:Nnn #1 {left} { \l_tmpa_dim } } - \dim_set:Nn \l_tmpa_dim { \ebproof_mark:Nn #1 {axis} - + \ebproof_mark:Nn #2 {right} - \ebproof_mark:Nn #2 {axis} } - \dim_compare:nNnT { \l_tmpa_dim } > { \ebproof_mark:Nn #1 {right} } { - \ebproof_set_mark:Nnn #1 {right} { \l_tmpa_dim } } -} - - -%%% Building blocks - -% Make a tree with explicit material in horizontal mode. Set the left and -% right marks to extremal positions and set the axis in the middle. - -\cs_new:Nn \ebproof_make_simple:Nn { - \hbox_set:Nn #1 { #2 } - \ebproof_set_mark:Nnn #1 { left } { 0pt } - \ebproof_set_mark:Nnn #1 { axis } { \box_wd:N #1 / 2 } - \ebproof_set_mark:Nnn #1 { right } { \box_wd:N #1 } -} - -% Make a tree with explicit material in horizontal mode, split in two parts. -% Set the left and right marks to extremal positions and set the axis between -% the two parts. - -\cs_new:Nn \ebproof_make_split:Nnn { - \ebproof_set_mark:Nnn #1 { left } { 0pt } - \hbox_set:Nn #1 { #2 } - \ebproof_set_mark:Nnn #1 { axis } { \box_wd:N #1 } - \hbox_set:Nn #1 { \hbox_unpack:N #1 #3 } - \ebproof_set_mark:Nnn #1 { right } { \box_wd:N #1 } -} - -% Make a tree with explicit material in vertical mode, using an explicit width -% and axis. - -\cs_new:Nn \ebproof_make_vertical:Nnnn { - \ebproof_set_mark:Nnn #1 { left } { 0pt } - \ebproof_set_mark:Nnn #1 { axis } { #2 } - \ebproof_set_mark:Nnn #1 { right } { #3 } - \vbox_set:Nn #1 { - \dim_set:Nn \tex_hsize:D { \ebproof_mark:Nn #1 {right} } +\cs_new:Nn \__ebproof_enlarge_conclusion:NN { + \dim_set:Nn \l_tmpa_dim { \__ebproof_mark:Nn #1 {axis} + + \__ebproof_mark:Nn #2 {left} - \__ebproof_mark:Nn #2 {axis} } + \dim_compare:nNnT { \l_tmpa_dim } < { \__ebproof_mark:Nn #1 {left} } { + \__ebproof_set_mark:Nnn #1 {left} { \l_tmpa_dim } } + \dim_set:Nn \l_tmpa_dim { \__ebproof_mark:Nn #1 {axis} + + \__ebproof_mark:Nn #2 {right} - \__ebproof_mark:Nn #2 {axis} } + \dim_compare:nNnT { \l_tmpa_dim } > { \__ebproof_mark:Nn #1 {right} } { + \__ebproof_set_mark:Nnn #1 {right} { \l_tmpa_dim } } +} +\cs_new:Nn \__ebproof_make_simple:Nn { + \hbox_set:cn { \__ebproof_box:N #1 } { #2 } + \__ebproof_set_mark:Nnn #1 { left } { 0pt } + \__ebproof_set_mark:Nnn #1 { axis } { \box_wd:c { \__ebproof_box:N #1 } / 2 } + \__ebproof_set_mark:Nnn #1 { right } { \box_wd:c { \__ebproof_box:N #1 } } +} +\cs_new:Nn \__ebproof_make_split:Nnn { + \__ebproof_set_mark:Nnn #1 { left } { 0pt } + \hbox_set:cn { \__ebproof_box:N #1 } { #2 } + \__ebproof_set_mark:Nnn #1 { axis } { \box_wd:c { \__ebproof_box:N #1 } } + \hbox_set:cn { \__ebproof_box:N #1 } { \hbox_unpack:c { \__ebproof_box:N #1 } #3 } + \__ebproof_set_mark:Nnn #1 { right } { \box_wd:c { \__ebproof_box:N #1 } } +} +\cs_new:Nn \__ebproof_make_vertical:Nnnn { + \__ebproof_set_mark:Nnn #1 { left } { 0pt } + \__ebproof_set_mark:Nnn #1 { axis } { #2 } + \__ebproof_set_mark:Nnn #1 { right } { #3 } + \vbox_set:cn { \__ebproof_box:N #1 } { + \dim_set:Nn \tex_hsize:D { \__ebproof_mark:Nn #1 {right} } #4 } - \box_set_wd:Nn #1 { \ebproof_mark:Nn #1 {right} } -} - -%%% Assembling boxes - -% Extend a tree box. The marks are shifted so that alignment is preserved. The -% arguments are dimensions for the left, top, right and bottom sides -% respectively. - -\cs_new:Nn \ebproof_extend:Nnnnn { + \box_set_wd:cn { \__ebproof_box:N #1 } { \__ebproof_mark:Nn #1 {right} } +} +\cs_new:Nn \__ebproof_extend:Nnnnn { \dim_compare:nNnF { #2 } = { 0pt } { - \hbox_set:Nn #1 { + \hbox_set:cn { \__ebproof_box:N #1 } { \skip_horizontal:n { #2 } - \box_use:N #1 + \box_use:c { \__ebproof_box:N #1 } } - \ebproof_shift_x:Nn #1 { #2 } + \__ebproof_shift_x:Nn #1 { #2 } } - \box_set_ht:Nn #1 { \box_ht:N #1 + #3 } - \box_set_wd:Nn #1 { \box_wd:N #1 + #4 } - \box_set_dp:Nn #1 { \box_dp:N #1 + #5 } -} - -% Append the contents of the second tree to the first one on the right, with -% matching baselines. The marks of both trees are preserved. The middle -% argument specifies the space to insert between boxes. - -\cs_new:Nn \ebproof_append_right:NnN { - \hbox_set:Nn #1 { - \box_use:N #1 + \box_set_ht:Nn #1 { \box_ht:c { \__ebproof_box:N #1 } + #3 } + \box_set_wd:Nn #1 { \box_wd:c { \__ebproof_box:N #1 } + #4 } + \box_set_dp:Nn #1 { \box_dp:c { \__ebproof_box:N #1 } + #5 } +} +\cs_new:Nn \__ebproof_append_right:NnN { + \hbox_set:cn { \__ebproof_box:N #1 } { + \box_use:c { \__ebproof_box:N #1 } \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } } - \box_use:N #3 + \box_use:c { \__ebproof_box:N #3 } } } - -% Append the contents of the second tree to the first one on the left, with -% matching baselines. The marks of the first tree are shifted accordingly. The -% middle argument specifies the space to insert between boxes. - -\cs_new:Nn \ebproof_append_left:NnN { - \ebproof_shift_x:Nn #1 { \box_wd:N #3 + #2 } - \hbox_set:Nn #1 { - \box_use:N #3 +\cs_new:Nn \__ebproof_append_left:NnN { + \__ebproof_shift_x:Nn #1 { \box_wd:c { \__ebproof_box:N #3 } + #2 } + \hbox_set:cn { \__ebproof_box:N #1 } { + \box_use:c { \__ebproof_box:N #3 } \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } } - \box_use:N #1 + \box_use:c { \__ebproof_box:N #1 } } } - -% Shift of two trees to the right so that the axes match. The marks of the one -% that is shifted are updated accordingly. - -\cs_new:Nn \ebproof_align:NN { +\cs_new:Nn \__ebproof_align:NN { \dim_set:Nn \l_tmpa_dim - { \ebproof_mark:Nn #2 {axis} - \ebproof_mark:Nn #1 {axis} } + { \__ebproof_mark:Nn #2 {axis} - \__ebproof_mark:Nn #1 {axis} } \dim_compare:nNnTF \l_tmpa_dim < { 0pt } { - \ebproof_extend:Nnnnn #2 { -\l_tmpa_dim } { 0pt } { 0pt } { 0pt } + \__ebproof_extend:Nnnnn #2 { -\l_tmpa_dim } { 0pt } { 0pt } { 0pt } } { - \ebproof_extend:Nnnnn #1 { \l_tmpa_dim } { 0pt } { 0pt } { 0pt } + \__ebproof_extend:Nnnnn #1 { \l_tmpa_dim } { 0pt } { 0pt } { 0pt } } } - -% Append the contents of the second tree above the first one, with matching -% axes. The marks of the first tree are preserved. - -\cs_new:Nn \ebproof_append_above:NN { - \ebproof_align:NN #1 #2 - \vbox_set:Nn #1 { - \box_use:N #2 +\cs_new:Nn \__ebproof_append_above:NN { + \__ebproof_align:NN #1 #2 + \vbox_set:cn { \__ebproof_box:N #1 } { + \box_use:c { \__ebproof_box:N #2 } \tex_prevdepth:D -1000pt - \box_use:N #1 + \box_use:c { \__ebproof_box:N #1 } } } - -% Append the contents of the second tree below the first one, with matching -% axes. The marks of the first tree are preserved. - -\cs_new:Nn \ebproof_append_below:NN { - \ebproof_align:NN #1 #2 +\cs_new:Nn \__ebproof_append_below:NN { + \__ebproof_align:NN #1 #2 \vbox_set_top:Nn #1 { - \box_use:N #1 + \box_use:c { \__ebproof_box:N #1 } \tex_prevdepth:D -1000pt - \box_use:N #2 + \box_use:c { \__ebproof_box:N #2 } } } - -% Shift the material in a tree vertically so that the height and depth are -% equal (like TeX's \vcenter but around the baseline). - -\cs_new:Nn \ebproof_vcenter:N { - \dim_set:Nn \l_tmpa_dim { ( \box_ht:N #1 - \box_dp:N #1 ) / 2 } - \box_set_eq:NN \l_tmpa_box #1 - \hbox_set:Nn #1 +\cs_new:Nn \__ebproof_overlay:NN { + \__ebproof_align:NN #1 #2 + \hbox_set:cn { \__ebproof_box:N #1 } { + \hbox_overlap_right:n { \box_use:c { \__ebproof_box:N #1 } } + \box_use:c { \__ebproof_box:N #2 } + \dim_compare:nNnT + { \box_wd:c { \__ebproof_box:N #2 } } < { \box_wd:c { \__ebproof_box:N #1 } } + { \skip_horizontal:n + { \box_wd:c { \__ebproof_box:N #1 } - \box_wd:c { \__ebproof_box:N #2 } } } + } +} +\cs_new:Nn \__ebproof_vcenter:N { + \dim_set:Nn \l_tmpa_dim + { ( \box_ht:c { \__ebproof_box:N #1 } - \box_dp:c { \__ebproof_box:N #1 } ) / 2 } + \box_set_eq:Nc \l_tmpa_box { \__ebproof_box:N #1 } + \hbox_set:cn { \__ebproof_box:N #1 } { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_tmpa_box } } } - - -%% Making inferences -% -% The following commands use the parameters defined at the beginning of the -% package for actually building proof trees using the commands defined above. - -% Append the contents of the second tree above or below the first one, -% depending on current settings. Axes are aligned and the marks of the first -% tree are preserved. - -\cs_new:Nn \ebproof_append_vertical:NN { - \bool_if:NTF \l_ebproof_updown_bool - { \ebproof_append_below:NN #1 #2 } - { \ebproof_append_above:NN #1 #2 } -} - -% Make a box containing an inference rule with labels, using the current -% settings. The width and axis position are taken as those of the conclusion -% of another tree box. The third argument is used as a temporary register for -% building labels. - -\cs_new:Nn \ebproof_make_rule_for:NNN { - - % Build the rule. - - \ebproof_make_vertical:Nnnn #1 - { \ebproof_mark:Nn #2 {axis} - \ebproof_mark:Nn #2 {left} } - { \ebproof_mark:Nn #2 {right} - \ebproof_mark:Nn #2 {left} } +\cs_new:Nn \__ebproof_append_vertical:NN { + \bool_if:NTF \l__ebproof_updown_bool + { \__ebproof_append_below:NN #1 #2 } + { \__ebproof_append_above:NN #1 #2 } +} +\cs_new:Nn \__ebproof_make_rule_for:NNN { + \__ebproof_make_vertical:Nnnn #1 + { \__ebproof_mark:Nn #2 {axis} - \__ebproof_mark:Nn #2 {left} } + { \__ebproof_mark:Nn #2 {right} - \__ebproof_mark:Nn #2 {left} } { - \skip_vertical:N \l_ebproof_rule_margin_dim - \tl_if_empty:NF { \l_ebproof_rule_code_tl } { - \tl_use:N \l_ebproof_rule_code_tl - \skip_vertical:N \l_ebproof_rule_margin_dim + \skip_vertical:N \l__ebproof_rule_margin_dim + \tl_if_empty:NF { \l__ebproof_rule_code_tl } { + \tl_use:N \l__ebproof_rule_code_tl + \skip_vertical:N \l__ebproof_rule_margin_dim } } - \ebproof_vcenter:N #1 - - % Append the left label - - \tl_if_blank:VF \l_ebproof_left_label_tl { - \ebproof_make_simple:Nn #3 { - \box_move_down:nn { \l_ebproof_label_axis_dim } { \hbox:n { - \cs_set_eq:NN \inserttext \l_ebproof_left_label_tl - \tl_use:N \l_ebproof_left_label_template_tl + \__ebproof_vcenter:N #1 + \tl_if_blank:VF \l__ebproof_left_label_tl { + \__ebproof_make_simple:Nn #3 { + \box_move_down:nn { \l__ebproof_label_axis_dim } { \hbox:n { + \cs_set_eq:NN \inserttext \l__ebproof_left_label_tl + \tl_use:N \l__ebproof_left_label_template_tl } } } - \box_set_ht:Nn #3 { 0pt } - \box_set_dp:Nn #3 { 0pt } - \ebproof_append_left:NnN - \l_ebproof_c_box \l_ebproof_label_separation_dim \l_ebproof_d_box + \box_set_ht:cn { \__ebproof_box:N #3 } { 0pt } + \box_set_dp:cn { \__ebproof_box:N #3 } { 0pt } + \__ebproof_append_left:NnN + \l__ebproof_c_box \l__ebproof_label_separation_dim \l__ebproof_d_box } - - % Append the right label - - \tl_if_blank:VF \l_ebproof_right_label_tl { - \ebproof_make_simple:Nn #3 { - \box_move_down:nn { \l_ebproof_label_axis_dim } { \hbox:n { - \cs_set_eq:NN \inserttext \l_ebproof_right_label_tl - \tl_use:N \l_ebproof_right_label_template_tl + \tl_if_blank:VF \l__ebproof_right_label_tl { + \__ebproof_make_simple:Nn #3 { + \box_move_down:nn { \l__ebproof_label_axis_dim } { \hbox:n { + \cs_set_eq:NN \inserttext \l__ebproof_right_label_tl + \tl_use:N \l__ebproof_right_label_template_tl } } } - \box_set_ht:Nn #3 { 0pt } - \box_set_dp:Nn #3 { 0pt } - \ebproof_append_right:NnN - \l_ebproof_c_box \l_ebproof_label_separation_dim \l_ebproof_d_box + \box_set_ht:cn { \__ebproof_box:N #3 } { 0pt } + \box_set_dp:cn { \__ebproof_box:N #3 } { 0pt } + \__ebproof_append_right:NnN + \l__ebproof_c_box \l__ebproof_label_separation_dim \l__ebproof_d_box } - -} - - -%% Stack-based interface - -%%% The stack - -% Logically, box structures are stored on a stack. However, TeX does not -% provide data structures for that and the grouping mechanism is not flexible -% enough, so we encode them using what we actually have. A stack for boxes is -% implemented using a global hbox |\g_ebproof_stack_box| that contains all the -% boxes successively. A sequence |\g_ebproof_stack_seq| is used to store the -% dimensions property lists textually. We maintain a counter -% |\g_ebproof_level_int| with the number of elements on the stack, for -% consistency checks. - -\int_new:N \g_ebproof_level_int -\box_new:N \g_ebproof_stack_box -\seq_new:N \g_ebproof_stack_seq - -% Clear the stack. - -\cs_new:Nn \ebproof_clear_stack: { - \int_gset:Nn \g_ebproof_level_int { 0 } - \hbox_gset:Nn \g_ebproof_stack_box { } - \seq_gclear:N \g_ebproof_stack_seq -} - -% Push the contents of a register on the stack. - -\cs_new:Nn \ebproof_push:N { - \int_gincr:N \g_ebproof_level_int - \hbox_gset:Nn \g_ebproof_stack_box - { \hbox_unpack:N \g_ebproof_stack_box \box_use:N #1 } - \seq_gput_left:Nv \g_ebproof_stack_seq - { l_ebproof_marks_ \__int_value:w #1 _prop } -} - -% Pop the value from the top of the stack into a register. - -\cs_new:Nn \ebproof_pop:N { - \int_compare:nNnTF { \g_ebproof_level_int } > { 0 } { - \int_gdecr:N \g_ebproof_level_int - \hbox_gset:Nn \g_ebproof_stack_box { - \hbox_unpack:N \g_ebproof_stack_box +} +\int_new:N \g__ebproof_level_int +\box_new:N \g__ebproof_stack_box +\seq_new:N \g__ebproof_stack_seq +\cs_new:Nn \__ebproof_clear_stack: { + \int_gset:Nn \g__ebproof_level_int { 0 } + \hbox_gset:Nn \g__ebproof_stack_box { } + \seq_gclear:N \g__ebproof_stack_seq +} +\cs_new:Nn \__ebproof_push:N { + \int_gincr:N \g__ebproof_level_int + \hbox_gset:Nn \g__ebproof_stack_box + { \hbox_unpack:N \g__ebproof_stack_box \box_use:c { \__ebproof_box:N #1 } } + \seq_gput_left:Nv \g__ebproof_stack_seq + { \__ebproof_marks:N #1 } +} +\cs_new:Nn \__ebproof_pop:N { + \int_compare:nNnTF { \g__ebproof_level_int } > { 0 } { + \int_gdecr:N \g__ebproof_level_int + \hbox_gset:Nn \g__ebproof_stack_box { + \hbox_unpack:N \g__ebproof_stack_box \box_gset_to_last:N \g_tmpa_box } - \box_set_eq_clear:NN #1 \g_tmpa_box - \seq_gpop_left:NN \g_ebproof_stack_seq \l_tmpa_tl - \tl_set_eq:cN { l_ebproof_marks_ \__int_value:w #1 _prop } \l_tmpa_tl + \box_set_eq_clear:cN { \__ebproof_box:N #1 } \g_tmpa_box + \seq_gpop_left:NN \g__ebproof_stack_seq \l_tmpa_tl + \tl_set_eq:cN { \__ebproof_marks:N #1 } \l_tmpa_tl } { \PackageError{ebproof}{Missing~premiss~in~a~proof~tree}{} - \ebproof_clear:N #1 + \__ebproof_clear:N #1 } } - -%%% Assembling trees - -\ebproof_new:N \l_ebproof_a_box -\ebproof_new:N \l_ebproof_b_box -\ebproof_new:N \l_ebproof_c_box -\ebproof_new:N \l_ebproof_d_box - -% Join horizontally a number of elements at the top of the stack. If several -% trees are joined, use the left mark of the left tree, the right mark of the -% right tree and set the axis in the middle of these marks. - -\cs_new:Nn \ebproof_join_horizontal:n { +\__ebproof_new:N \l__ebproof_a_box +\__ebproof_new:N \l__ebproof_b_box +\__ebproof_new:N \l__ebproof_c_box +\__ebproof_new:N \l__ebproof_d_box +\cs_new:Nn \__ebproof_join_horizontal:n { \int_case:nnF { #1 } { { 0 } { \group_begin: - \ebproof_clear:N \l_ebproof_a_box - \ebproof_push:N \l_ebproof_a_box + \__ebproof_clear:N \l__ebproof_a_box + \__ebproof_push:N \l__ebproof_a_box \group_end: } { 1 } { } } { \group_begin: - \ebproof_pop:N \l_ebproof_a_box + \__ebproof_pop:N \l__ebproof_a_box \prg_replicate:nn { #1 - 1 } { - \ebproof_pop:N \l_ebproof_b_box - \ebproof_append_left:NnN - \l_ebproof_a_box \l_ebproof_separation_dim \l_ebproof_b_box + \__ebproof_pop:N \l__ebproof_b_box + \__ebproof_append_left:NnN + \l__ebproof_a_box \l__ebproof_separation_dim \l__ebproof_b_box } - \ebproof_set_mark:Nnn \l_ebproof_a_box { left } - { \ebproof_mark:Nn \l_ebproof_b_box { left } } - \ebproof_set_mark:Nnn \l_ebproof_a_box { axis } - { ( \ebproof_mark:Nn \l_ebproof_a_box { left } - + \ebproof_mark:Nn \l_ebproof_a_box { right } ) / 2 } - \ebproof_push:N \l_ebproof_a_box + \__ebproof_set_mark:Nnn \l__ebproof_a_box { left } + { \__ebproof_mark:Nn \l__ebproof_b_box { left } } + \__ebproof_set_mark:Nnn \l__ebproof_a_box { axis } + { ( \__ebproof_mark:Nn \l__ebproof_a_box { left } + + \__ebproof_mark:Nn \l__ebproof_a_box { right } ) / 2 } + \__ebproof_push:N \l__ebproof_a_box \group_end: } } - -% Join vertically the two elements at the top of the stack, with a horizontal -% rule of the appropriate size. - -\cs_new:Nn \ebproof_join_vertical: { +\cs_new:Nn \__ebproof_join_vertical: { \group_begin: - \ebproof_pop:N \l_ebproof_a_box - \ebproof_pop:N \l_ebproof_b_box - \ebproof_enlarge_conclusion:NN \l_ebproof_b_box \l_ebproof_a_box - \ebproof_make_rule_for:NNN \l_ebproof_c_box \l_ebproof_b_box - \l_ebproof_d_box - \ebproof_append_vertical:NN \l_ebproof_a_box \l_ebproof_c_box - \ebproof_append_vertical:NN \l_ebproof_a_box \l_ebproof_b_box - \ebproof_push:N \l_ebproof_a_box + \__ebproof_pop:N \l__ebproof_a_box + \__ebproof_pop:N \l__ebproof_b_box + \__ebproof_enlarge_conclusion:NN \l__ebproof_b_box \l__ebproof_a_box + \__ebproof_make_rule_for:NNN \l__ebproof_c_box \l__ebproof_b_box + \l__ebproof_d_box + \__ebproof_append_vertical:NN \l__ebproof_a_box \l__ebproof_c_box + \__ebproof_append_vertical:NN \l__ebproof_a_box \l__ebproof_b_box + \__ebproof_push:N \l__ebproof_a_box \group_end: } - -%%% High-level commands - -% Push a box with default formatting, using explicit alignment if the code -% contains a |&| character - -\cs_new:Npn \ebproof_statement_parse:w #1\ebproof_statement_stop: { +\cs_new:Npn \__ebproof_statement_parse:w #1 & #2 & #3 \q_stop { \tl_if_empty:nTF { #3 } { - \ebproof_make_simple:Nn \l_ebproof_a_box - { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_ebproof_template_tl } + \__ebproof_make_simple:Nn \l__ebproof_a_box + { \cs_set:Npn \inserttext { #1 } \tl_use:N \l__ebproof_template_tl } } { - \ebproof_make_split:Nnn \l_ebproof_a_box - { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_ebproof_left_template_tl } - { \cs_set:Npn \inserttext { #2 } \tl_use:N \l_ebproof_right_template_tl } + \__ebproof_make_split:Nnn \l__ebproof_a_box + { \cs_set:Npn \inserttext { #1 } \tl_use:N \l__ebproof_left_template_tl } + { \cs_set:Npn \inserttext { #2 } \tl_use:N \l__ebproof_right_template_tl } } - \ebproof_push:N \l_ebproof_a_box -} - -\cs_new:Nn \ebproof_push_statement:n { - \ebproof_statement_parse:w #1&& \ebproof_statement_stop: -} - - -%% Document interface - -%%% Functions to define statements - -% The |\g_ebproof_stack_seq| variable contains the list of all defined -% statements. For each statement |X|, there is a document command |\ebproofX| -% and the alias |\X| is defined when entering a |prooftree| environment. - -\seq_new:N \g_ebproof_statements_seq - -% Install the aliases for statements, saving the original value of the control -% sequences. - -\cs_new:Nn \ebproof_setup_statements: { - \seq_map_inline:Nn \g_ebproof_statements_seq { + \__ebproof_push:N \l__ebproof_a_box +} +\cs_new:Nn \__ebproof_push_statement:n { + \__ebproof_statement_parse:w #1 & & \q_stop +} +\seq_new:N \g__ebproof_statements_seq +\cs_new:Nn \__ebproof_setup_statements: { + \seq_map_inline:Nn \g__ebproof_statements_seq { \cs_set_eq:cc { ebproof_saved_ ##1 } { ##1 } \cs_set_eq:cc { ##1 } { ebproof ##1 } } } - -% Restore the saved meanings of the control sequences. This is useful when -% interpreting user-provided code in statement arguments. The meanings are -% automatically restored when leaving a |prooftree| environment because of -% grouping. - -\cs_new:Nn \ebproof_restore_statements: { - \seq_map_inline:Nn \g_ebproof_statements_seq { +\cs_new:Nn \__ebproof_restore_statements: { + \seq_map_inline:Nn \g__ebproof_statements_seq { \cs_set_eq:cc { ##1 } { ebproof_saved_ ##1 } } } - -% Define a new statement. The first argument is the name, the second one is an -% argument specifier as used by |xparse| and the third one is the body of the -% command. - -\cs_new:Nn \ebproof_new_statement:nnn { +\cs_new:Nn \__ebproof_new_statement:nnn { \exp_args:Nc \NewDocumentCommand { ebproof#1 }{ #2 } { #3 } - \seq_put_right:Nn \g_ebproof_statements_seq { #1 } -} - -% Define a deprecated statement. The syntax is the same as above except that -% an extra argument in third position indicates what should be used instead. -% The effect is the same except that a warning message is issued the first -% time the statement is used. - -\cs_new:Nn \ebproof_new_deprecated_statement:nnnn { + \seq_put_right:Nn \g__ebproof_statements_seq { #1 } +} +\cs_new:Nn \__ebproof_new_deprecated_statement:nnnn { \cs_new:cpn { ebproof_#1_warning: } { \PackageWarning { ebproof } { \token_to_str:c{#1}~is~deprecated,~#3 } \cs_gset:cn { ebproof_#1_warning: } { } } - \ebproof_new_statement:nnn { #1 } { #2 } + \__ebproof_new_statement:nnn { #1 } { #2 } { \use:c { ebproof_#1_warning: } #4 } } - - -%%% Basic commands - -\ebproof_new_statement:nnn { set } { m } { +\__ebproof_new_statement:nnn { set } { m } { \keys_set:nn { ebproof } { #1 } } - -\ebproof_new_statement:nnn { hypo } { O{} m } { +\__ebproof_new_statement:nnn { hypo } { O{} m } { \group_begin: - \ebproof_restore_statements: + \__ebproof_restore_statements: \keys_set:nn { ebproof } { #1 } - \ebproof_push_statement:n { #2 } + \__ebproof_push_statement:n { #2 } \group_end: } - -\ebproof_new_statement:nnn { infer } { O{} m O{} m } { +\__ebproof_new_statement:nnn { infer } { O{} m O{} m } { \group_begin: - \ebproof_restore_statements: + \__ebproof_restore_statements: \keys_set_known:nnN { ebproof / rule~style } { #1 } \l_tmpa_tl \keys_set:nV { ebproof } \l_tmpa_tl - \tl_set:Nn \l_ebproof_right_label_tl { #3 } - \ebproof_join_horizontal:n { #2 } - \ebproof_push_statement:n { #4 } - \ebproof_join_vertical: + \tl_set:Nn \l__ebproof_right_label_tl { #3 } + \__ebproof_join_horizontal:n { #2 } + \__ebproof_push_statement:n { #4 } + \__ebproof_join_vertical: \group_end: } - -\ebproof_new_statement:nnn { ellipsis } { m m } { +\__ebproof_new_statement:nnn { ellipsis } { m m } { \group_begin: - \ebproof_restore_statements: - \tl_clear:N \l_ebproof_rule_code_tl - \ebproof_make_split:Nnn \l_ebproof_a_box { } { + \__ebproof_restore_statements: + \tl_clear:N \l__ebproof_rule_code_tl + \__ebproof_make_split:Nnn \l__ebproof_a_box { } { \vbox_set:Nn \l_tmpa_box { \skip_vertical:n { 1.2ex } \hbox:n { \tex_ignorespaces:D #1 } @@ -651,117 +428,103 @@ label~axis .dim_set:N = \l_ebproof_label_axis_dim, } \hbox_overlap_right:n { ~ \box_use:N \l_tmpa_box } } - \ebproof_push:N \l_ebproof_a_box - \ebproof_join_vertical: - \ebproof_push_statement:n {#2} - \ebproof_join_vertical: + \__ebproof_push:N \l__ebproof_a_box + \__ebproof_join_vertical: + \__ebproof_push_statement:n {#2} + \__ebproof_join_vertical: \group_end: } - - -%%% Modifying trees - -% Rewrite the box at the top of the stack while preserving its dimensions an -% marks. The code is typeset in horizontal mode, with control sequences to -% access the original box and its marks: -% - \treebox is a box register with the original material -% - \treemark{NAME} provides the value of a given mark - -\ebproof_new_statement:nnn { rewrite } { m } { +\__ebproof_new_statement:nnn { rewrite } { m } { \group_begin: - \ebproof_restore_statements: - \ebproof_pop:N \l_ebproof_a_box - \box_set_eq:NN \l_tmpa_box \l_ebproof_a_box + \__ebproof_restore_statements: + \__ebproof_pop:N \l__ebproof_a_box + \box_set_eq:Nc \l_tmpa_box { \__ebproof_box:N \l__ebproof_a_box } \hbox_set:Nn \l_tmpb_box { \cs_set_eq:NN \treebox \l_tmpa_box - \cs_set:Npn \treemark { \ebproof_mark:Nn \l_ebproof_a_box } + \cs_set:Npn \treemark { \__ebproof_mark:Nn \l__ebproof_a_box } { #1 } } - \box_set_wd:Nn \l_tmpb_box { \box_wd:N \l_ebproof_a_box } - \box_set_ht:Nn \l_tmpb_box { \box_ht:N \l_ebproof_a_box } - \box_set_dp:Nn \l_tmpb_box { \box_dp:N \l_ebproof_a_box } - \box_set_eq:NN \l_ebproof_a_box \l_tmpb_box - \ebproof_push:N \l_ebproof_a_box + \box_set_wd:Nn \l_tmpb_box { \box_wd:c { \__ebproof_box:N \l__ebproof_a_box } } + \box_set_ht:Nn \l_tmpb_box { \box_ht:c { \__ebproof_box:N \l__ebproof_a_box } } + \box_set_dp:Nn \l_tmpb_box { \box_dp:c { \__ebproof_box:N \l__ebproof_a_box } } + \box_set_eq:cN { \__ebproof_box:N \l__ebproof_a_box } \l_tmpb_box + \__ebproof_push:N \l__ebproof_a_box \group_end: } - -% Insert |\left| and |\right| delimiters without changing the alignment - -\ebproof_new_statement:nnn { delims } { m m } { +\__ebproof_new_statement:nnn { delims } { m m } { \group_begin: - \ebproof_restore_statements: - \ebproof_pop:N \l_ebproof_a_box + \__ebproof_restore_statements: + \__ebproof_pop:N \l__ebproof_a_box \hbox_set:Nn \l_tmpa_box - { $ \tex_vcenter:D { \box_use:N \l_ebproof_a_box } $ } + { $ \tex_vcenter:D { \box_use:c { \__ebproof_box:N \l__ebproof_a_box } } $ } \dim_set:Nn \l_tmpa_dim - { \box_ht:N \l_tmpa_box - \box_ht:N \l_ebproof_a_box } - \hbox_set:Nn \l_ebproof_a_box { + { \box_ht:N \l_tmpa_box - \box_ht:c { \__ebproof_box:N \l__ebproof_a_box } } + \hbox_set:cn { \__ebproof_box:N \l__ebproof_a_box } { $ #1 \tex_vrule:D height \box_ht:N \l_tmpa_box depth \box_dp:N \l_tmpa_box width 0pt \tex_right:D . $ } - \ebproof_shift_x:Nn \l_ebproof_a_box { \box_wd:N \l_ebproof_a_box } - \hbox_set:Nn \l_ebproof_a_box { - \hbox_unpack:N \l_ebproof_a_box + \__ebproof_shift_x:Nn \l__ebproof_a_box + { \box_wd:c { \__ebproof_box:N \l__ebproof_a_box } } + \hbox_set:cn { \__ebproof_box:N \l__ebproof_a_box } { + \hbox_unpack:c { \__ebproof_box:N \l__ebproof_a_box } $ \tex_left:D . \box_use:N \l_tmpa_box #2 $ } - \hbox_set:Nn \l_ebproof_a_box - { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_ebproof_a_box } } - \ebproof_push:N \l_ebproof_a_box + \hbox_set:cn { \__ebproof_box:N \l__ebproof_a_box } + { \box_move_down:nn { \l_tmpa_dim } + { \box_use:c { \__ebproof_box:N \l__ebproof_a_box } } } + \__ebproof_push:N \l__ebproof_a_box + \group_end: +} +\__ebproof_new_statement:nnn { overlay } { } { + \group_begin: + \__ebproof_pop:N \l__ebproof_a_box + \__ebproof_pop:N \l__ebproof_b_box + \__ebproof_overlay:NN \l__ebproof_a_box \l__ebproof_b_box + \__ebproof_push:N \l__ebproof_a_box \group_end: } - - -%%% Deprecated statements - -% These statements were defined in versions 1.x of the package, they are -% preserved for temporary upwards compatibility and will be removed in a -% future version. - -\ebproof_new_deprecated_statement:nnnn { Alter } { m } +\__ebproof_new_deprecated_statement:nnnn { Alter } { m } { use~\token_to_str:c{rewrite}~instead } { \ebproofrewrite{ #1 \box\treebox } } -\ebproof_new_deprecated_statement:nnnn { Delims } { } +\__ebproof_new_deprecated_statement:nnnn { Delims } { } { use~\token_to_str:c{delims}~instead } { \ebproofdelims } -\ebproof_new_deprecated_statement:nnnn { Ellipsis } { } +\__ebproof_new_deprecated_statement:nnnn { Ellipsis } { } { use~\token_to_str:c{ellipsis}~instead } { \ebproofellipsis } -\ebproof_new_deprecated_statement:nnnn { Hypo } { } +\__ebproof_new_deprecated_statement:nnnn { Hypo } { } { use~\token_to_str:c{hypo}~instead } { \ebproofhypo } -\ebproof_new_deprecated_statement:nnnn { Infer } { } +\__ebproof_new_deprecated_statement:nnnn { Infer } { } { use~\token_to_str:c{infer}~instead } { \ebproofinfer } - - -%%% Environment interface - -\ebproof_clear_stack: - -\tl_new:N \l_ebproof_start_level_tl - +\__ebproof_clear_stack: +\tl_new:N \l__ebproof_start_level_tl \NewDocumentEnvironment { prooftree } { s O{} } { + \group_align_safe_begin: \keys_set_known:nnN { ebproof / proof~style } { #2 } \l_tmpa_tl \keys_set:nV { ebproof } \l_tmpa_tl - \tl_set:Nx \l_ebproof_start_level_tl { \int_use:N \g_ebproof_level_int } + \tl_set:Nx \l__ebproof_start_level_tl { \int_use:N \g__ebproof_level_int } \vbox_set:Nw \l_tmpa_box - \ebproof_setup_statements: + \__ebproof_setup_statements: } { \vbox_set_end: - \ebproof_pop:N \l_ebproof_a_box - \int_compare:nNnF { \g_ebproof_level_int } = { \tl_use:N \l_ebproof_start_level_tl } { + \__ebproof_pop:N \l__ebproof_a_box + \int_compare:nNnF { \g__ebproof_level_int } = { \tl_use:N \l__ebproof_start_level_tl } { \PackageError{ebproof}{Malformed~proof~tree}{ Some~hypotheses~were~declared~but~not~used~in~this~tree.} } \IfBooleanTF { #1 } { - \[ \box_use:N \l_ebproof_a_box \] + \[ \box_use:c { \__ebproof_box:N \l__ebproof_a_box } \] \ignorespacesafterend } { \hbox_unpack:N \c_empty_box - \bool_if:NTF \l_ebproof_center_bool { - \hbox:n { $ \tex_vcenter:D { \box_use:N \l_ebproof_a_box } $ } + \bool_if:NTF \l__ebproof_center_bool { + \hbox:n { $ \tex_vcenter:D { \box_use:c { \__ebproof_box:N \l__ebproof_a_box } } $ } } { - \box_use:N \l_ebproof_a_box + \box_use:c { \__ebproof_box:N \l__ebproof_a_box } } } + \group_align_safe_end: } - -% A trick for the starred version: \cs_new:cpn { prooftree* } { \prooftree* } \cs_new:cpn { endprooftree* } { \endprooftree } +\endinput +%% +%% End of file `ebproof.sty'. -- cgit v1.2.3