% \iffalse
%<*driver>
\def\stexdocpath{../../doc}
\input{\stexdocpath/stex-docheader}
\stextoptitle{The \sTeX Package}{stex}
\docmodule
%</driver>
%<*package>
% \fi
%
% \begin{sfragment}{Proofs}
%
% \begin{implementation}
%    \begin{macrocode}
%<@@=stex_proof>
%    \end{macrocode}
%
% Keys:
%    \begin{macrocode}

\stex_keys_define:nnnn{ spfcommon }{
  \tl_clear:N \l_stex_key_for_clist
  \tl_clear:N \l_stex_key_term_tl
  \tl_clear:N \l_stex_key_method_tl
  \tl_clear:N \l_stex_key_just_tl
}{
  for         .clist_set:N  = \l_stex_key_for_clist ,
  term        .tl_set:N     = \l_stex_key_term_tl,
  method      .tl_set:N     = \l_stex_key_method_tl,
  just        .tl_set:N     = \l_stex_key_just_tl,
}{id,style,title}

\bool_set_false:N \l_stex_key_showname_bool

\stex_keys_define:nnnn{ spfnamed }{
  \str_clear:N \l_stex_key_name_str
  \str_clear:N \l_stex_key_numname_str
  \bool_set_false:N \l_stex_key_showname_bool
}{
  name        .str_set_x:N  = \l_stex_key_name_str,
  numname     .str_set_x:N  = \l_stex_key_numname_str,
  showname    .bool_set:N   = \l_stex_key_showname_bool
}{spfcommon}

\cs_new_protected:Nn \_@@_do_spf_name: {
  \str_if_empty:NTF \l_stex_key_numname_str {
    \str_if_empty:NTF \l_stex_key_name_str {
      \bool_set_false:N \l_stex_key_showname_bool
    } {
      \exp_args:Nne\use:nn{\vardef}{{v\l_stex_key_name_str}[name=\l_stex_key_name_str]{\l_stex_key_name_str}}
    }
  }{
    \bool_set_false:N \l_stex_key_showname_bool
    \_@@_number_as_string:N \l_@@_counter_str
    \exp_args:Nne \use:nn {\vardef}{{\l_stex_key_numname_str}[name=\l_@@_counter_str]{\l_@@_counter_str}}
  }
}

\cs_new_protected:Nn \_@@_do_spf_name_i: {
  \str_if_empty:NTF \l_@@_key_numname_str {
    %\str_if_empty:NF \l_@@_key_name_str {
      \exp_args:Nne\use:nn{\vardef}{{v\l_@@_key_name_str}[name=\l_@@_key_name_str]{\l_@@_key_name_str}}
    %}
  }{
    \exp_args:Nne \use:nn {\vardef}{{\l_@@_key_numname_str}[name=\l_@@_counter_str]{\l_@@_counter_str}}
  }
}

\cs_new_protected:Nn \_@@_do_spf_varname: {
  \bool_if:NT \l_stex_key_showname_bool {
    ~($\csname v\l_stex_key_name_str\endcsname$)~
  }
}

\stex_keys_define:nnnn{ spftop }{
  \tl_set_eq:NN \l_stex_key_proofend_tl \_@@_proof_box_tl
  \bool_set_false:N \l_stex_key_hide_bool
  \tl_clear:N \l_stex_key_continues_tl
  \tl_clear:N \l_stex_key_functions_tl
  \tl_clear:N \l_stex_key_from_tl
}{
  proofend    .tl_set:N     = \l_stex_key_proofend_tl,
  hide        .code:n       = {
    \str_if_eq:eeT{#1}{true}{
      \bool_set_true:N \l_stex_key_hide_bool
    }
  },
  continues   .tl_set:N     = \l_stex_key_continues_tl, % <- unused
  functions   .tl_set:N     = \l_stex_key_functions_tl, % <- unused
  from        .tl_set:N     = \l_stex_key_from_tl % <- unused
}{spfcommon}

\stex_keys_define:nnnn{ subproof }{}{}{spftop,spfnamed}

\bool_set_true:N \l_@@_inc_counter_bool
%    \end{macrocode}
%
% For proofs, we will have to have deeply nested structures of enumerated list-like
% environments. However, {\LaTeX} only allows |enumerate| environments up to nesting depth
% 4 and general list environments up to listing depth 6. This is not enough for us.
% Therefore we have decided to go along the route proposed by Leslie Lamport to use a
% single top-level list with dotted sequences of numbers to identify the position in the
% proof tree. Unfortunately, we could not use his |pf.sty| package directly, since it does
% not do automatic numbering, and we have to add keyword arguments all over the place, to
% accomodate semantic information.
%
%    \begin{macrocode}
\intarray_new:Nn\l_@@_counter_intarray{50}

\cs_new_protected:Npn \_@@_insert_number: {
  \int_set:Nn \l_tmpa_int {1}
  \bool_while_do:nn {
    \int_compare_p:nNn {
      \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
    } > 0
  }{
    \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int .
    \int_incr:N \l_tmpa_int
  }
}
\cs_new_protected:Nn \_@@_number_as_string:N {
  \str_clear:N #1
  \int_set:Nn \l_tmpa_int {1}
  \bool_while_do:nn {
    \int_compare_p:nNn {
      \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
    } > 0
  }{
    \str_put_right:Ne #1 {\intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int .}
    \int_incr:N \l_tmpa_int
  }
}

\cs_new_protected:Npn \_@@_inc_counter: {
  \int_set:Nn \l_tmpa_int {1}
  \bool_while_do:nn {
    \int_compare_p:nNn {
      \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
    } > 0
  }{
    \int_incr:N \l_tmpa_int
  }
  \int_compare:nNnF \l_tmpa_int = 1 {
    \int_decr:N \l_tmpa_int
  }
  \intarray_gset:Nnn \l_@@_counter_intarray \l_tmpa_int {
    \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int + 1
  }
}

\cs_new_protected:Npn \_@@_add_counter: {
  \int_set:Nn \l_tmpa_int {1}
  \bool_while_do:nn {
    \int_compare_p:nNn {
      \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
    } > 0
  }{
    \int_incr:N \l_tmpa_int
  }
  \intarray_gset:Nnn \l_@@_counter_intarray \l_tmpa_int { 1 }
}

\cs_new_protected:Npn \_@@_remove_counter: {
  \int_set:Nn \l_tmpa_int {1}
  \bool_while_do:nn {
    \int_compare_p:nNn {
      \intarray_item:Nn \l_@@_counter_intarray \l_tmpa_int
    } > 0
  }{
    \int_incr:N \l_tmpa_int
  }
  \int_decr:N \l_tmpa_int
  \intarray_gset:Nnn \l_@@_counter_intarray \l_tmpa_int { 0 }
}
%    \end{macrocode}
%
% \end{implementation}
%
% \begin{senvironment}{sproof}
%
% \StartImpl
%    \begin{macrocode}
\bool_set_false:N \l_@@_in_spfblock_bool

\cs_new_protected:Nn \_@@_begin_proof:nn {\par
  \intarray_gzero:N \l_@@_counter_intarray
  \intarray_gset:Nnn \l_@@_counter_intarray 1 1
  \stex_keys_set:nn{spftop}{#1}
  \_stex_do_for_list:
  \stex_if_do_html:T {
    \_@@_html_env_proof:
  }
  \seq_map_inline:Nn \l_stex_fors_seq {
    \stex_debug:nn{definiens}{Adding~definiens~to~##1}
    \stex_if_do_html:TF{
      \STEXinvisible{\hbox{\_stex_add_definiens:nn {##1}{proven}}}
    }{
      \_stex_add_definiens:nn {##1}{\STEXinvisible{proven}}
    }
  }
  \stex_if_do_html:F\stex_style_apply:
  %\_stex_do_id:
  \stex_reactivate_macro:N \subproof
  \stex_reactivate_macro:N \spfstep
  \stex_reactivate_macro:N \conclude
  \stex_reactivate_macro:N \assumption
  \stex_reactivate_macro:N \eqstep
  \stex_reactivate_macro:N \yield
  \stex_reactivate_macro:N \spfescape
  \stex_reactivate_macro:N \spfblock
  \stex_reactivate_macro:N \spfjust
  \stex_reactivate_macro:N \spfby
  \stex_reactivate_macro:N \spfarg
  \noindent\stex_annotate:nn{data-ftml-title={}}{\_stex_annotate_force_break:n{#2}}\par
  \stex_if_do_html:TF{
    \use:c{stex_annotate_env}{data-ftml-proofbody={}}
    \_stex_annotate_force_break:n{}
  }{
    \bool_if:NT \l_stex_key_hide_bool{\setbox0\vbox\bgroup}
  }
}

\cs_new_protected:Nn \_@@_html_env_proof: {
  \exp_args:Nne \use:c{stex_annotate_env}{
    data-ftml-proof={}
    \seq_if_empty:NF \l_stex_fors_seq {,
      data-ftml-fors={\seq_map_indexed_function:NN \l_stex_fors_seq \_stex_comma_sep_uri:nn }
    }
    \bool_if:NT \l_stex_key_hide_bool {,
      data-ftml-proofhide=true
    }
  }
  \_@@_html:
}

\cs_new_protected:Nn \_@@_html_env_subproof: {
  \str_if_empty:NF \l_stex_key_numname_str {
    \_@@_number_as_string:N \l_@@_counter_str
  }
  \exp_args:Nne \use:c{stex_annotate_env}{
    data-ftml-subproof={}
    \seq_if_empty:NF \l_stex_fors_seq {,
      data-ftml-fors={\seq_map_indexed_function:NN \l_stex_fors_seq \_stex_comma_sep_uri:nn }
    }
    \bool_if:NT \l_stex_key_hide_bool {,
      data-ftml-proofhide=true
    }
    \str_if_empty:NTF \l_stex_key_numname_str {
      \str_if_empty:NF \l_stex_key_name_str {,
        data-ftml-stepname={\l_stex_key_name_str}
      }
    }{
      , data-ftml-stepname={\l_@@_counter_str}
    }
  }
  \_@@_html:
}

\cs_new_protected:Nn \_@@_html: {
  \_stex_annotate_force_break:n{}
  \tl_set:Ne\l_tmpa_tl {\l_stex_key_term_tl\l_stex_key_method_tl\l_stex_key_just_tl}
  \tl_if_empty:NF\l_tmpa_tl{
    \stex_annotate_invisible:n{\hbox{
      \tl_if_empty:NF \l_stex_key_term_tl {
        $\stex_annotate:nn{data-ftml-proofterm={}}{\l_stex_key_term_tl}$
      }
      \tl_if_empty:NF \l_stex_key_just_tl {
        $\stex_annotate:nn{data-ftml-spfjust={}}{\l_stex_key_just_tl}$
      }
      \tl_if_empty:NF \l_stex_key_method_tl {
        \stex_annotate:nn{data-ftml-proofmethod={}}{\l_stex_key_method_tl}
      }
    }}
  }
}

\cs_new_protected:Nn \_@@_start_comment: {
  \bool_if:NT \l_@@_in_spfblock_bool {
    \par
    \group_begin:\stexcommentfont 
  }
}
\cs_new_protected:Nn \_@@_end_comment: {
  \bool_if:NT \l_@@_in_spfblock_bool { 
    \par
    \group_end: 
  }
}
\cs_new_protected:Npn \spfescape #1{
  \_@@_end_comment: #1 \_@@_start_comment:
}
\stex_deactivate_macro:Nn \spfescape {sproof~environments}

\stex_new_stylable_env:nnnnnnn{proof}{O{} m}{
  \_@@_begin_proof:nn{#1}{#2}
  \bool_set_true:N\l_@@_in_spfblock_bool
  %\_@@_start_list:n{}
  \_@@_start_comment:
}{
  \stex_if_do_html:TF{
    %\_@@_end_list:
    \use:c{endstex_annotate_env}\use:c{endstex_annotate_env}
  }\stex_style_apply:
}{
  \emph{\sproofautorefname :}~
}{
  \sproofend
}{s}

\AddToHook{env/sproof/end}{
  \_@@_end_comment:
  \stex_if_do_html:F{\bool_if:NT \l_stex_key_hide_bool\egroup}
}


\stex_new_stylable_env:nnnnnnn{proof*}{O{}}{
  \_@@_begin_proof:nn{#1}{}
  \bool_set_false:N\l_@@_in_spfblock_bool
}{
  \stex_if_do_html:TF{\use:c{endstex_annotate_env}\use:c{endstex_annotate_env}}\stex_style_apply:
}{
  \emph{Proof:}~
}{
  \sproofend
}{s}

\cs_new_protected:Nn \_@@_start_list:n {
  %\par
  \group_begin:\list{}{
    \setlength\topsep{0pt}
    \setlength\parsep{0pt}
    \setlength\rightmargin{0pt}
  }\item[#1]
}

\cs_new_protected:Nn \_@@_end_list: {
  %\par
  \endlist\group_end:
}
%    \end{macrocode}
% \end{senvironment}
%
% \begin{senvironment}{subproof}
%
% \StartImpl
%    \begin{macrocode}
\str_set_eq:NN \subproofautorefname \spfstepautorefname

\cs_new_protected:Nn \_@@_do_after_subproof:N {
  \bgroup
    \expandafter \_@@_do_after_subproof_i:nn #1
  \egroup
  \_@@_do_spf_name_i:
}
\cs_new_protected:Nn \_@@_do_after_subproof_i:nn {
    \exp_args:Nno \stex_keys_set:nn{subproof}{#1}
    \str_gset_eq:NN \l_@@_key_name_str \l_stex_key_name_str
    \str_gset_eq:NN \l_@@_key_numname_str \l_stex_key_numname_str
    \bool_gset_eq:NN \l_@@_key_showname_bool \l_stex_key_showname_bool
    \str_gset:Nn \l_@@_counter_str {#2}
}
\cs_new_protected:Npn \_@@_set_after_subproof:n {
  \str_if_empty:NTF \l_stex_key_numname_str {
    \str_if_empty:NTF \l_stex_key_name_str \use_none:n \_@@_set_after_subproof_i:n
  }\_@@_set_after_subproof_i:n
}
\cs_new_protected:Npn \_@@_set_after_subproof_with_number:n {
  \str_if_empty:NTF \l_stex_key_numname_str {
    \str_if_empty:NTF \l_stex_key_name_str \use_none:n \_@@_set_after_subproof_with_number_i:n
  }\_@@_set_after_subproof_with_number_i:n
}
\cs_new_protected:Nn \_@@_set_after_subproof_i:n {
  \tl_gset:cn{subproof_arg_ \int_use:N \currentgrouplevel}{{#1}{}}

  \_@@_set_aftergroup: % \bool_if:NTF \l_@@_in_spfblock_bool \_@@_set_aftergroup: \_@@_set_aftergroup_double:
}
\cs_new_protected:Nn \_@@_set_after_subproof_with_number_i:n {
  \_@@_number_as_string:N \l_@@_counter_str
  \tl_gset:ce{subproof_arg_ \int_use:N \currentgrouplevel}{{\exp_not:n{#1}}{\l_@@_counter_str}}
  \_@@_set_aftergroup:
}
\cs_new_protected:Nn \_@@_set_aftergroup: {
    \aftergroup \_@@_do_after_subproof:N
    \expandafter \aftergroup \csname subproof_arg_ \int_use:N \currentgrouplevel\endcsname
}

\stex_new_stylable_env:nnnnnnn{subproof}{s O{} m}{
  \stex_keys_set:nn{subproof}{#2}
  \_stex_do_for_list:
  \stex_if_do_html:T {
    \_@@_html_env_subproof:
  }
  \seq_map_inline:Nn \l_stex_fors_seq {
    \stex_debug:nn{definiens}{Adding~definiens~to~##1}
    \stex_if_do_html:TF{
      \STEXinvisible{\hbox{\_stex_add_definiens:nn {##1}{proven}}}
    }{
      \_stex_add_definiens:nn {##1}{\STEXinvisible{proven}}
    }
  }

  \IfBooleanTF #1 {
    \bool_set_false:N \l_@@_in_spfblock_bool
    \_@@_set_after_subproof:n{#2}
    \stex_if_do_html:F \stex_style_apply:
    \str_if_empty:NF \l_stex_key_id_str {
      \_@@_number_as_string:N \@currentlabel
      %\str_set:Ne \@currentHref{subproof.\@currentlabel}
      %\_stex_do_id:
    }


    \stex_annotate:nn{data-ftml-title={}}{#3}
  }{
    \bool_if:NTF \l_@@_in_spfblock_bool {
      
      \_@@_set_after_subproof_with_number:n{#2}

      %\str_if_empty:NF \l_stex_key_id_str {
        %\_@@_number_as_string:N \@currentlabel
        %\str_set:Ne \@currentHref{subproof.\@currentlabel}
        %\_stex_do_id:
      %}
      \use:c{stex_annotate_env}{data-ftml-title={}} \_@@_start_list:n{\_@@_insert_number:\_@@_do_spf_varname:} #3 \par \use:c{endstex_annotate_env}
        \_@@_add_counter:
        \stex_if_do_html:F \stex_style_apply:
    }{
      \noindent \stex_annotate:nn{data-ftml-title={}}{#3} \par
      \stex_if_do_html:F \stex_style_apply:

      \_@@_set_after_subproof:n{#2}

      %\_stex_do_id:
    }
  }
  \stex_if_do_html:TF{
    \use:c{stex_annotate_env}{data-ftml-proofbody={}}
    \_stex_annotate_force_break:n{}
  }{\bool_if:NT \l_stex_key_hide_bool{\setbox0\vbox\bgroup}}
  \_@@_start_comment:
}{
  \bool_if:NT\l_@@_in_spfblock_bool {
    \_@@_remove_counter: 
    \_@@_inc_counter:
  }

  \stex_if_do_html:TF{
    \use:c{endstex_annotate_env} %proofbody
    \bool_if:NT\l_@@_in_spfblock_bool \_@@_end_list:
    \use:c{endstex_annotate_env} % subproof
  }{
    \stex_style_apply:
    \bool_if:NT \l_@@_in_spfblock_bool \_@@_end_list:
  }
}{}{}{}

\AddToHook{env/subproof/before}{
  \_@@_end_comment:
}

\AddToHook{env/subproof/after}{
  \_@@_start_comment:
}

\AddToHook{env/subproof/end}{
  \_@@_end_comment:
  \stex_if_do_html:F{\bool_if:NT \l_stex_key_hide_bool\egroup}
}

\stex_deactivate_macro:Nn \subproof {sproof~environments}

%    \end{macrocode}
% \end{senvironment}
%
% \begin{senvironment}{spfsketchenv}
%
% \StartImpl
% TODO:
%    \begin{macrocode}
\newenvironment{spfsketchenv}{}{}
%    \end{macrocode}
% \end{senvironment}
%
% \begin{sfunction}{\spfsketch}{}
%
% \StartImpl
%    \begin{macrocode}
\stex_new_stylable_cmd:nnnn{spfsketch}{O{} m}{\par
  \begin{spfsketchenv}
  \stex_keys_set:nn{spftop}{#1}
  \_stex_do_for_list:
  \_stex_do_id:
  \par
  \exp_args:Nne \use:c{stex_annotate_env}{
    data-ftml-proofsketch={
      \seq_if_empty:NF \l_stex_fors_seq {
        \seq_map_function:NN \l_stex_fors_seq \stex_use_symbol_uri:N
      }
    }
  }
    \stex_style_apply:
    #2\par
    \use:c{endstex_annotate_env}
  \end{spfsketchenv}
}{
  \noindent\emph{\spfsketchenvautorefname :}~
}
%    \end{macrocode}
% \end{sfunction}
%
% \begin{implementation}
% Keys for proof step macros:
%    \begin{macrocode}
\stex_keys_define:nnnn { spfsteps } {
  %\str_clear:N \l_stex_key_name_str
}{
  %name        .str_set_x:N  = \l_stex_key_name_str
}{spfcommon,spfnamed}
%    \end{macrocode}
%
% Common setup for all the proof step macros:
%    \begin{macrocode}
\cs_new_protected:Nn \_@@_make_step_macro:Nnnnn {
  \NewDocumentCommand #1 {s O{} +m} {
    \_@@_end_comment:
    \stex_keys_set:nn{spfsteps}{##2}
    %\str_if_empty:NF \l_stex_key_name_str {
    %  \exp_args:Nne\use:nn{\vardef}{{v\l_stex_key_name_str}[name=\l_stex_key_name_str]{\l_stex_key_name_str}}
    %}
    \_@@_do_spf_name:

    \spfstepenv
    \str_if_empty:NF \l_stex_key_id_str {
      %\_@@_number_as_string:N \@currentlabel
      %\str_set:Ne \@currentHref{spfstep.\@currentlabel}
      %\_stex_do_id:
    }

    \bool_if:NTF \l_@@_in_spfblock_bool { 
      \IfBooleanTF ##1 {
        \_@@_step_html_i:nn{#2}{##3}
      }{
        \_@@_step_html:nn{#2}{\_@@_start_list:n{#3} ##3 \_@@_end_list:}
        #5
      }
      \endspfstepenv
      \_@@_start_comment:
    }{
      \_@@_step_html_i:nn{#2}{##3}
      \endspfstepenv
    }
  }
  \stex_deactivate_macro:Nn #1 {sproof~environments}
}

\cs_new_protected:Nn \_@@_step_html:nn {
  \str_if_empty:NF \l_stex_key_numname_str {
    \_@@_number_as_string:N \l_@@_counter_str
  }
  \stex_if_do_html:TF{
    %\group_begin:
    \exp_args:Nne \use:c{stex_annotate_env}{
      data-ftml-spf#1={
        \seq_if_empty:NF \l_stex_fors_seq {
          \seq_map_function:NN \l_stex_fors_seq \stex_use_symbol_uri:N
        }
      }
      \str_if_empty:NTF \l_stex_key_numname_str {
        \str_if_empty:NF \l_stex_key_name_str {,
          data-ftml-stepname={\l_stex_key_name_str}
        }
      }{
        , data-ftml-stepname={\l_@@_counter_str}
      }
    }
    \_@@_html:
    #2 
    \par
    \use:c{endstex_annotate_env}
    %\group_end:
  }{ #2 }
}
\cs_new_protected:Nn \_@@_step_html_i:nn {
  \stex_if_do_html:TF{
    \noindent
    %\group_begin:
    \exp_args:Ne \stex_annotate:nn{
      data-ftml-spf#1={
        \seq_if_empty:NF \l_stex_fors_seq {
          \seq_map_function:NN \l_stex_fors_seq \stex_use_symbol_uri:N
        }
      }
      \str_if_empty:NTF \l_stex_key_numname_str {
        \str_if_empty:NF \l_stex_key_name_str {,
          data-ftml-stepname={\l_stex_key_name_str}
        }
      }{
        , data-ftml-stepname={\l_@@_counter_str}
      }
    }{
      \_@@_html:
      #2 
    }
    %\group_end:
  }{ #2 }
}
%    \end{macrocode}
%
% \end{implementation}
%
% \begin{senvironment}{spfstepenv}
% \StartImpl
% TODO:
%    \begin{macrocode}
\newenvironment{spfstepenv}{
  \str_set_eq:NN \spfstepenvautorefname \spfstepautorefname
}{}
%    \end{macrocode}
% \end{senvironment}
%
% \begin{senvironment}{spfblock}
% \StartImpl
%    \begin{macrocode}
\NewDocumentEnvironment{spfblock}{}{
  \bool_set_false:N \l_@@_in_spfblock_bool
}{
  \aftergroup\_@@_start_comment:
}

\stex_deactivate_macro:Nn \spfblock {sproof~environments}
\AddToHook{env/spfblock/before}{
  \_@@_end_comment:
}
%    \end{macrocode}
% \end{senvironment}
%
% \begin{sfunction}{\spfstep}{}
% \StartImpl
%    \begin{macrocode}
\_@@_make_step_macro:Nnnnn \spfstep {step} {\_@@_insert_number:\_@@_do_spf_varname:} {} \_@@_inc_counter:
%    \end{macrocode}
% \end{sfunction}
%
% \begin{sfunction}{\assumption}{}
% \StartImpl
%    \begin{macrocode}
\_@@_make_step_macro:Nnnnn \assumption {assumption} {\_@@_insert_number:\_@@_do_spf_varname:} {} \_@@_inc_counter:
%    \end{macrocode}
% \end{sfunction}
%
% \begin{sfunction}{\conclude}{}
% \StartImpl
%    \begin{macrocode}
\_@@_make_step_macro:Nnnnn \conclude {conclusion} {$\Rightarrow$} {} {}
%    \end{macrocode}
% \end{sfunction}
%
% \begin{sfunction}{\eqstep}{}
% \StartImpl
%    \begin{macrocode}
\NewDocumentCommand \eqstep {s m}{
  \_@@_end_comment:
  \spfstepenv

  \bool_if:NTF \l_@@_in_spfblock_bool {
    \IfBooleanTF #1 {
      \_@@_step_html_i:nn{eqstep}{$= #2$}
    }{
      \_@@_step_html:nn{eqstep}{\_@@_start_list:n{$=$} $#2$ \_@@_end_list:}
    }
    \endspfstepenv
    \_@@_start_comment:
  }{
    \_@@_step_html_i:nn{eqstep}{$= #2$}
    \endspfstepenv
  }
}
\stex_deactivate_macro:Nn \eqstep {sproof~environments}
%    \end{macrocode}
% \end{sfunction}
%
% \begin{sfunction}{\yield}{}
% \StartImpl
%    \begin{macrocode}
\NewDocumentCommand \yield {+m}{
  \stex_annotate:nn{data-ftml-proofterm={}}{ #1 }
}
\stex_deactivate_macro:Nn \yield {sproof~environments}
%    \end{macrocode}
% \end{sfunction}
%
% \begin{sfunction}{\spfjust}{}
% \StartImpl
%    \begin{macrocode}
\newcommand\spfjust[1]{
  \stex_annotate:nn{data-ftml-spfjust={}}{ #1 }
}
\stex_deactivate_macro:Nn \spfjust {sproof~environments}
%    \end{macrocode}
% \end{sfunction}
%
% \begin{sfunction}{\spfby}{}
% \StartImpl
%    \begin{macrocode}
\newcommand\spfby[1]{
  \stex_annotate:nn{data-ftml-proofmethod={}}{ #1 }
}
\stex_deactivate_macro:Nn \spfby {sproof~environments}
%    \end{macrocode}
% \end{sfunction}
%
% \begin{sfunction}{\spfarg}{}
% \StartImpl
%    \begin{macrocode}
\newcommand\spfarg[2][]{
  \stex_annotate:nn{data-ftml-spfarg={#1}}{ #2 }
}
\stex_deactivate_macro:Nn \spfarg {sproof~environments}
%    \end{macrocode}
% \end{sfunction}
%
%
% \begin{sfunction}{\sproofend}{}
%
% \StartImpl
%    \begin{macrocode}
\tl_set:Nn \_@@_proof_box_tl {
  \ltx@ifpackageloaded{amssymb}{$\square$}{
    \hbox{\vrule\vbox{\hrule width 6 pt\vskip 6pt\hrule}\vrule}
  }
}

\tl_set:Nn \sproofend {
  \tl_if_empty:NF \l_stex_key_proofend_tl {
    \hfil\null\nobreak\hfill\l_stex_key_proofend_tl\par\smallskip
  }
}
%    \end{macrocode}
% \end{sfunction}
%
% \begin{sfunction}{\stexcommentfont}{}
%
% \StartImpl
%    \begin{macrocode}
\cs_new_protected:Npn \stexcommentfont {
  \small\itshape
}
%    \end{macrocode}
% \end{sfunction}
%
% \end{sfragment}