%% %% 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}{2021/01/28}{2.1.1}{EB's proof trees} \bool_new:N \l__ebproof_updown_bool \keys_define:nn { ebproof } { 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, 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:, 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 } } \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 } } \ebproofnewrulestyle { dashed } { rule~code = { \hbox_to_wd:nn { \tex_hsize:D } { \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 \skip_horizontal:N \l_tmpa_dim } \tex_hfill:D \skip_horizontal:n { -\l_tmpa_dim } } } } \keys_set:nn { ebproof } { center = true, proof~style = upwards, separation = 1.5em, rule~margin = .7ex, rule~thickness = .4pt, rule~separation = 2pt, rule~dash~length = .2em, rule~dash~space = .3em, rule~style = simple, template = $\inserttext$, left~template = $\inserttext\mathrel{}$, right~template = $\mathrel{}\inserttext$, left~label = , right~label = , left~label~template = \inserttext, right~label~template = \inserttext, label~separation = 0.5em, label~axis = 0.5ex } \NewDocumentCommand \ebproofnewstyle { mm } { \keys_define:nn { ebproof } { #1 .meta:n = { #2 } } } \int_new:N \g__ebproof_register_int \cs_new:Nn \__ebproof_box:N { \str_item:nn { #1 } { 2 } __ebproof_ \tl_use:N #1 _box } \cs_new:Nn \__ebproof_marks:N { \str_item:nn { #1 } { 2 } __ebproof_ \tl_use:N #1 _prop } \cs_new:Nn \__ebproof_new:N { \tl_new:N #1 \int_gincr:N \g__ebproof_register_int \str_if_eq:eeTF { \str_item:nn { #1 } { 2 } } { g } { \tl_gset:Nx #1 { \int_to_arabic:n { \g__ebproof_register_int } } } { \tl_set: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 } } } \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:cn { \__ebproof_box:N #1 } { \__ebproof_mark:Nn #1 {right} } } \cs_new:Nn \__ebproof_extend:Nnnnn { \dim_compare:nNnF { #2 } = { 0pt } { \hbox_set:cn { \__ebproof_box:N #1 } { \skip_horizontal:n { #2 } \box_use:c { \__ebproof_box:N #1 } } \__ebproof_shift_x:Nn #1 { #2 } } \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:c { \__ebproof_box: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:c { \__ebproof_box:N #1 } } } \cs_new:Nn \__ebproof_align:NN { \dim_set:Nn \l_tmpa_dim { \__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 #1 { \l_tmpa_dim } { 0pt } { 0pt } { 0pt } } } \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:c { \__ebproof_box:N #1 } } } \cs_new:Nn \__ebproof_append_below:NN { \__ebproof_align:NN #1 #2 \vbox_set_top:cn { \__ebproof_box:N #1 } { \box_use:c { \__ebproof_box:N #1 } \tex_prevdepth:D -1000pt \box_use:c { \__ebproof_box:N #2 } } } \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 } } } \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 } } \__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: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 } \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: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 } } \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_drop: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_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 \group_end: } { 1 } { } } { \group_begin: \__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_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: } } \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 \group_end: } \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_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 & & \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 } } } \cs_new:Nn \__ebproof_restore_statements: { \seq_map_inline:Nn \g__ebproof_statements_seq { \cs_set_eq:cc { ##1 } { ebproof_saved_ ##1 } } } \cs_new:Nn \__ebproof_new_statement:nnn { \exp_args:Nc \NewDocumentCommand { ebproof#1 }{ #2 } { #3 } \seq_gput_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 } { \use:c { ebproof_#1_warning: } #4 } } \__ebproof_new_statement:nnn { set } { m } { \keys_set:nn { ebproof } { #1 } } \__ebproof_new_statement:nnn { hypo } { O{} m } { \group_begin: \__ebproof_restore_statements: \keys_set:nn { ebproof } { #1 } \__ebproof_push_statement:n { #2 } \group_end: } \__ebproof_new_statement:nnn { infer } { O{} m O{} m } { \group_begin: \__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: \group_end: } \__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 { } { \vbox_set:Nn \l_tmpa_box { \skip_vertical:n { 1.2ex } \hbox:n { \tex_ignorespaces:D #1 } \skip_vertical:n { 1.2ex } } \vbox_to_ht:nn { \box_ht:N \l_tmpa_box } { \tex_xleaders:D \vbox_to_ht:nn { .8ex } { \tex_vss:D \hbox:n { . } \tex_vss:D } \tex_vfill:D } \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: \group_end: } \__ebproof_new_statement:nnn { rewrite } { m } { \group_begin: \__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 } { #1 } } \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: } \__ebproof_new_statement:nnn { delims } { m m } { \group_begin: \__ebproof_restore_statements: \__ebproof_pop:N \l__ebproof_a_box \hbox_set:Nn \l_tmpa_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: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: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: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: } \__ebproof_new_deprecated_statement:nnnn { Alter } { m } { use~\token_to_str:c{rewrite}~instead } { \ebproofrewrite{ #1 \box\treebox } } \__ebproof_new_deprecated_statement:nnnn { Delims } { } { use~\token_to_str:c{delims}~instead } { \ebproofdelims } \__ebproof_new_deprecated_statement:nnnn { Ellipsis } { } { use~\token_to_str:c{ellipsis}~instead } { \ebproofellipsis } \__ebproof_new_deprecated_statement:nnnn { Hypo } { } { use~\token_to_str:c{hypo}~instead } { \ebproofhypo } \__ebproof_new_deprecated_statement:nnnn { Infer } { } { use~\token_to_str:c{infer}~instead } { \ebproofinfer } \__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 } \vbox_set:Nw \l_tmpa_box \__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 } { \PackageError{ebproof}{Malformed~proof~tree}{ Some~hypotheses~were~declared~but~not~used~in~this~tree.} } \IfBooleanTF { #1 } { \[ \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:c { \__ebproof_box:N \l__ebproof_a_box } } $ } } { \box_use:c { \__ebproof_box:N \l__ebproof_a_box } } } \group_align_safe_end: } \cs_new:cpn { prooftree* } { \prooftree* } \cs_new:cpn { endprooftree* } { \endprooftree } \endinput %% %% End of file `ebproof.sty'.