% \iffalse meta-comment
%
%% File: propositions.dtx
%%
%% Copyright (C) 2026 Cian Dorr
%%
%% This work may be distributed and/or modified under the
%% conditions of the LaTeX Project Public License, either version 1.3c
%% of this license or (at your option) any later version.
%% The latest version of this license is in
%%
%%    https://www.latex-project.org/lppl.txt
%%
%% and version 1.3c or later is part of all distributions of LaTeX
%% version 2008 or later.
%%
%% This work has the LPPL maintenance status `maintained'.
%%
%% The Current Maintainer of this work is Cian Dorr.
%%
%% This work consists of the files propositions.dtx and propositions.ins
%% and the derived files propositions.sty and propositions.pdf.
%%
% \fi
%
% \iffalse
%<*driver>
\documentclass[leqno]{ltxdoc}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage[most]{tcolorbox}
\tcbuselibrary{documentation}
\usepackage[equations]{propositions}
\usepackage{cleveref}
\usepackage{fancyvrb}
\VerbatimFootnotes

\hypersetup{colorlinks,linkcolor=blue!60!black,urlcolor=blue!60!black}

%% Live examples: the code above, its result below, in a two-tone tcolorbox.
%% The body is written out verbatim and then used twice --- listed with
%% gobble=2, which strips the "% " that every documentation line carries, and
%% \input to produce the result (there % is still catcode 9, so it needs no
%% stripping).  fancyvrb does the listing rather than tcolorbox's own
%% \dispExample because listings' gobble is silently ignored by
%% \lstinputlisting, which is what \dispExample uses.
\newenvironment{example}
  {\VerbatimEnvironment
   \begin{VerbatimOut}{\jobname-ex.tex}}
  {\end{VerbatimOut}%
   \begin{tcolorbox}[propexample]
     \VerbatimInput[gobble=2]{\jobname-ex.tex}%
   \tcblower
     \input{\jobname-ex.tex}%
   \end{tcolorbox}}

%% Code-only display (no execution): the same box without a lower part.
\newenvironment{codebox}
  {\VerbatimEnvironment
   \begin{VerbatimOut}{\jobname-cb.tex}}
  {\end{VerbatimOut}%
   \begin{tcolorbox}[propexample]
     \VerbatimInput[gobble=2]{\jobname-cb.tex}%
   \end{tcolorbox}}

\tcbset{
  color command=red!60!black,
  color key=green!50!black,
  %% ExampleFrame/ExampleBack are tcolorbox's own documentation colours.
  propexample/.style={
    enhanced, breakable,
    colframe=ExampleFrame, colback=ExampleBack,
    skin=bicolor, colbacklower=white,
    arc=1pt, boxrule=0.6pt,
    left=1em, right=1em, top=0.5em, bottom=0.5em,
    before skip=\medskipamount, after skip=\medskipamount,
    fontupper=\small, fontlower=\small,
  },
  docexample/.style={
    colframe=blue!50!black,
    colback=blue!3!white,
    before skip=\medskipamount,
    after skip=\medskipamount,
    fontlower=\small,
  },
}


\EnableCrossrefs
\CodelineIndex
\OnlyDescription
\begin{document}
  \DocInput{\jobname.dtx}
\end{document}
%</driver>
% \fi
%
% \GetFileInfo{propositions.sty}
%
% \title{The \textsf{propositions} package}
% \author{Cian Dorr\\ \texttt{ciandorr@gmail.com}}
% \date{\fileversion: \filedate}
%
% \maketitle
%
% \begin{abstract}
% \noindent The \textsf{propositions} package provides a key-value driven system
% for labelling propositions, theses, and premises in academic papers.
% Items may be given names like `(P)' or
% `Physicalism', or auto-numbered using different counters; all carry robust
% cross-references with configurable formatting.
% The package integrates with \textsf{amsmath}, \textsf{hyperref},
% and \textsf{cleveref}.
% \end{abstract}
%
% \tableofcontents
%
% \section{Introduction}
%
% In some academic disciplines (such as philosophy), it is common to have displayed propositions (examples, theses, premises,\ldots) with various kinds of labels.  A thesis might be referred to as `(P)' or `Physicalism'; the premises of an argument might be numbered as `P1', `P2', `P3', \ldots; or examples might be numbered consecutively over the course of a whole article.
%   Standard \LaTeX{} environments like |enumerate| can
% handle some of these cases, but cross-referencing is awkward:
% |\ref| produces a bare number or letter, and the author must manually
% add parentheses or other formatting at every point of reference.  The standard |description| environment, meanwhile, does not allow cross-referencing at all.
%
% The \textsf{propositions} package solves this by attaching formatting
% information to each label.  With an appropriate choice of style, |\item[P]| (inside \refEnv{prop}) is displayed
% as ``(P)'' and |\ref| automatically produces ``(P)'' as well---complete
% with parentheses and hyperlink.  The full
% key-value interface supports named items, numbered items, custom
% counters, glosses, shorthands, per-item format changes, changes to the list geometry, and styles.
%
% The \refCom{ptag} command (which requires \textsf{amsmath}) extends this to
% displayed math environments: an equation can be tagged with a
% proposition label instead of (or using) its equation number, and |\ref| to an equation will pick up its
% name or number with specified formatting.
% 
% \section{History}
% I wrote the ancestor to this package in the 90s
% while finishing my Ph.D. thesis, and used it in my own work but never documented or shared it.  This new 
% version is a thorough re-implementation in \LaTeX3,
% written in 2026 with very extensive help from Claude Code.  I 
% hope others will find it as useful as I have.
% 
% \section{Basic usage}
% Load with |\usepackage{propositions}| (see \autoref{sect:keys-global} below for valid package options).
%
% The |prop| environment generates a list of propositions, each introduced by |\item|.  |\item| with an optional argument gives a |description|-like label:
% \begin{example}
% \begin{prop}
%   \item[Physicalism] Everything is physical. \label{phys}
%   \item[Idealism] Everything is mental. \label{ideal}
% \end{prop}
% \end{example}
% Unlike the standard |description| environment, one can refer back to these propositions using the standard |\ref| command (or with new cross-referencing commands described in \cref{sect:xref}):
% \begin{example}
% \ref{phys} is more plausible than \ref{ideal}.
% \end{example}
% With no optional argument, |\item| will by default generate numbered items similar to |enumerate|, but with numbering that persists across the document:
% \begin{example}
% \begin{prop}
%   \item Every atom is physical. \label{atoms}
% \end{prop}
% \ref{phys} follows from the conjunction of \ref{atoms} and
% \begin{prop}
%   \item Everything is an atom. \label{atomism}
% \end{prop}
% \end{example}
% As with |enumerate|, the
% counter and formatting depend on the
% nesting level:
% \begin{example}
% \begin{prop}
%   \item \label{dual}
%   \begin{prop}
%     \item Some things are physical. \label{some}
%     \item Some things are not physical. \label{notall}
%   \end{prop}
% \end{prop}
% Without \ref{some}, \ref{dual} would be consistent
% with \ref{ideal}.
% \end{example}
%
% \section{Advanced usage}
% The format of the proposition labels, and of
% subsequent references, are both configurable using a key=value syntax (see \autoref{sect:keys} for the possible keys):
% \begin{example}
% \begin{prop}
%   \item[No Overlap,
%         align=flush,
%         display format=\textsc{#1},
%         ref format=\textit{#1}]
%     Nothing mental is physical. \label{incomp}
% \end{prop}
% Is \ref{incomp} consistent with \ref{phys}?
% \end{example}
% The prop environment can also take an optional argument with a list of keys:
% \begin{example}
% \begin{prop}[leftmargin=5em, format=[#1]]
%   \item Every mental thing is physical. 
% \end{prop}
% \end{example}
% Preset styles can be declared and used in place of a set of key-value pairs.  The package loads with a range of predefined styles (see \cref{sect:builtin-styles}).
% \begin{example}
% \begin{prop}
%   \item[Nihilism, style=thesis] There is nothing. \label{nihilism}
% \end{prop}
% Does \ref{nihilism} imply \ref{phys}, \ref{dual}, or both?  Discuss.
% \end{example}
% 
% Additional cross-referencing commands (see \cref{sect:xref}) include \refCom{nref} (strips formatting from reference) and \refCom{lastref} (refers to the most recent proposition, even if it lacked a label):
% \begin{example}
% \begin{prop}
%   \item[Mentality] \label{mental} Everything is mental.
%   \item[\nref{mental}*] Many things are mental.
% \end{prop}
% One may think \lastref\ more reasonable than \ref{mental}.
% \end{example}
% 
% When the package is loaded with |\usepackage[equations]{propositions}|, a first-level |\item| within \refEnv{prop} 
% will use the counter as equations.  (This looks better 
% with the |leqno| option to |\documentclass|.)
% \begin{example}
% \begin{equation}
%   \exists x (\text{Mental}(x) \wedge \text{Physical}(x)) \label{overlap}
% \end{equation}
% \ref{overlap} can be stated in English as \ref{overlap2}:
% \begin{prop}
%   \item Some things are both mental and physical.  \label{overlap2}
% \end{prop}
% \end{example}
% The \refCom{ptag} command (requires \textsf{amsmath})
% is a replacement for the standard |\tag| command
% that behaves just like an |\item| in a \refEnv{prop} 
% environment.
% \begin{example}
% \begin{equation} 
%   \ptag[Monism, \format=\textsc{#1}] \label{mon}
%   \exists x \forall y(y = x)
% \end{equation}
% Is \ref{mon} compatible with \ref{dual}?
% \end{example}
%
% \section{Basic environments and commands}
%
% \begin{docEnvironment}{prop}{\oarg{keys}}
%   Creates a displayed list of propositions.  It is a standard \LaTeX{} list, so by default its formatting will depend on the standard length parameters like \cs{itemsep} and \cs{topsep}, although these can be overridden by setting keys.
%
%   Within \refEnv{prop}, \cs{item} creates the propositions (see below).
%
%   The optional \meta{keys} argument can contain a list of keys, which will affect only the given environment (not any other \refEnv{prop} environments that may be nested within it).  
% 
% \end{docEnvironment}
%
% \begin{docEnvironment}{inlineprop}{\oarg{keys}}
%   Like \refEnv{prop}, but does not create a list.  Allows \cs{item} to be used outside list environments, e.g.\ for generating numbers at the beginning of paragraphs.  Steps the \texttt{prop} counter and increments the nesting level.  Accepts the same optional \meta{keys} as \refEnv{prop}.
% \end{docEnvironment}
%
% Within \refEnv{prop} and \refEnv{inlineprop}, \cs{item} is redefined to act as the proposition-item command.  Its optional argument is a comma-separated list of \meta{key}=\meta{value} pairs (see \autoref{sect:keys}).  A bare string without \texttt{=} is treated as a proposition name.
%
% When used without an optional argument (or without setting \refKey{name}, \refKey{counter}, or \refKey{style}), the style is determined by the \refKey{nameless style} key (\autoref{sect:keys}).  By default this is \texttt{numbered}, which dispatches by nesting depth to \texttt{levelone}, \texttt{leveltwo}, \ldots\ via \refCom{proplevelchoice}.
%
% \begin{docCommand}{ptag}{\oarg{keys}}
%   (Available only when \textsf{amsmath} is loaded.)  Works inside displayed math environments like \texttt{equation} and \texttt{align}.  Accepts the same keys as \cs{item} within \refEnv{prop}, except that \refKey{align} has no effect (since positioning is controlled by the tag placement system).
% 
% Any display math environment (|equation|, |align|, etc.) used inside \refEnv{prop} or \refEnv{inlineprop} automatically increments the nesting level for its duration, so that \cs{ptag} inside such an environment behaves as if it were one level deeper.
% \end{docCommand}
% 
% \begin{docCommand}{propoptions}{\marg{keys}}
%   Sets default keys (see \autoref{sect:keys}), which take effect for all subsequent uses of \refEnv{prop}, \refEnv{inlineprop}, |\item|, and \refCom{ptag} (within the current scope).
% \end{docCommand}
% 
% \begin{docCommand}{proplevelchoice}{\marg{item1, item2, \ldots}}
%   Picks the entry from the comma-separated list depending on the current nesting depth (1-indexed; last element will be used if the list is too short; empty entries are skipped).  At depth~0 (outside any \refEnv{prop} environment), returns the first entry.  
% 
% This macro can be used, for example, to set different list dimensions for different nesting levels (see \cref{sect:keys-dims}) or to create styles that produce different results depending on the nesting depth where they are used (see \cref{sect:styles}).
% \end{docCommand}
% 
% 
% Further commands are described below, especially in \cref{sect:xref} (cross-referencing) and \cref{sect:styles} (defining styles).
% 
% \section{Keys}\label{sect:keys}
% 
% \subsection{Item-level keys}\label{sect:keys-item}
%
% The keys listed in this subsection can be used in the following places: 
% \begin{itemize}
%   \item 
%    In the optional argument of |\item| or \refCom{ptag}: the key applies to that item only.
%   \item In the optional argument of \refEnv{prop} or \refEnv{inlineprop}: the key applies to every top-level |\item| within
% that environment, unless overridden by the |\item|'s own optional argument.  (If another \refEnv{prop} or \refEnv{inlineprop} environment is used inside this one, the key will 
% not apply to its |\item|s.)
%   \item In the argument of \refCom{propoptions}: the key 
% will apply to every subsequent |\item| or \refCom{ptag} (in the current group), unless overridden by that |\item|'s optional argument, or that 
% of its parent environment.
%   \item In the optional argument of |\usepackage{propositions}|: equivalent to \refCom{propoptions}, except that keys that require the |#| character cannot be set here, (due to a limitation in how \LaTeX\ processes options)  
%   \item With \refCom{SetPropStyle} or \refCom{DeclareNumberedStyle}, to
% add the key to a given style.  
% \end{itemize}
%
% \begin{docKey}{style}{=\meta{style}}{no default}
%   A style, equivalent to a preset collection of keys: see \cref{sect:styles} for details.  
% \end{docKey}
% 
% \begin{docKey}{name}{=\meta{text}}{no default}
%   The proposition's name.  A bare string (without \texttt{=}) is equivalent to \texttt{name=}\meta{text}.  (To be precise: if the optional argument contains no \texttt{=} at all, the whole of it is the name; otherwise, it is read as a key list, and any entry of it without an \texttt{=} is the name, so a bare name can be combined with other keys, as in |\item[No Overlap, align=flush]|.  In that case a name containing a comma must be braced---|\item[{Alpha, Beta}, align=flush]|---and a name containing an \texttt{=} needs the explicit \texttt{name=}|{|\meta{text}|}| form.)
% \end{docKey}
%
% \begin{docKey}{counter}{=\meta{name}}{no default}
%   Counter to use.  The counter is automatically stepped, and the item's \refKey{name} is set to \cs{the}\meta{name} (though this can be overridden by \refKey{counter format} or \refKey{name}).
% 
% Any counter can be used with \refKey{counter format}.  Special counters \docCounter{numpropii}, \docCounter{numpropiii}, \docCounter{numpropiv}, \docCounter{numpropv} are provided, whose values are automatically reset each time an |\item| is processed at a lower nesting level.  (There is also a counter \docCounter{numpropi} which does not automatically reset.) 
% \end{docKey}
%
% \begin{docKey}{counter format}{=\meta{template}}{no default}
%   How to display the counter value.  Use \texttt{\#1} for the counter name, e.g.\ \texttt{counter format=\string\roman\{\#1\}}.  When both this key and \refKey{counter} are set, this is used instead of \cs{the}\meta{counter} for generating the item's \refKey{name}.
% \end{docKey}
%
% \begin{docKey}{display format}{=\meta{template}}{no default}
%   Format for displaying the name or counter value in the proposition's label.  Use \texttt{\#1} for the argument, e.g.\ \texttt{display format=\string\textbf\{\#1\}}.  Does not affect cross-references.
% \end{docKey}
%
% \begin{docKey}{ref format}{=\meta{template}}{no default}
%   Format for subsequent cross-references to this proposition.  Use \texttt{\#1} for the argument, e.g.\ \texttt{ref format=\string\{(\#1)\}}.  Does not affect the display.
% \end{docKey}
%
% % \begin{docKey}{format}{=\meta{template}}{no default}
%   Shorthand for setting both \refKey{display format} and \refKey{ref format}.
% \end{docKey}
% 
% \begin{docKey}{shorthand}{=\meta{text}}{no default}
%   An abbreviation displayed after the name.  If present, the shorthand becomes the reference text: \cs{ref} produces the shorthand (formatted with \refKey{ref format}) rather than the full name.
% \end{docKey}
%
% \begin{example}
% \begin{prop}
%   \item[Global Physical Supervenience, shorthand=GPS] \label{global}
%   Every fact is entailed by some fact about 
%   the physical world.  
% \end{prop}    
% There are several interesting arguments for \ref{global}.
% \end{example}
% 
% \begin{docKey}{shorthand format}{=\meta{template}}{initially \texttt{\string~[\#1]}}
%   Format for displaying the shorthand in the label.
% \end{docKey}
%
% \begin{docKey}{gloss}{=\meta{text}}{no default}
%   A parenthetical gloss displayed after the name.  Does not affect cross-references.
% \end{docKey}
%
% \begin{example}
% \begin{prop}
%   \item[Humean Supervenience, gloss=after David Lewis]
%   Every fact is entailed by some fact about the 
%   fundamental properties and spatiotemporal relations
%   of points.
% \end{prop}
% \end{example}
% 
% \begin{docKey}{gloss format}{=\meta{template}}{initially \texttt{\string~(\#1)}}
%   Format for displaying the gloss in the label.
% \end{docKey}
%
% \begin{docKey}{label format}{=\meta{template}}{no default}
%   Format applied to the \emph{entire} assembled label, i.e.\ the name (after
%   \refKey{display format}), shorthand, and gloss together.  Use \texttt{\#1} for
%   the whole assembled text.  For example, \texttt{label format=\#1:}\ appends
%   a colon after the complete label.
% \end{docKey}
%
% \begin{docKey}{ref}{=\meta{text}}{no default}
%   Explicitly set the reference text, overriding what would be derived from \refKey{name}, \refKey{counter}, or \refKey{shorthand}.
% \end{docKey}
%
% \begin{docKey}{label}{=\meta{label}}{no default}
%   Equivalent to a trailing \cs{label}\marg{label}.
% \end{docKey}
%
% \begin{docKey}{reset}{=\meta{boolean}}{initially \texttt{true}}
%   When \texttt{true} (the default), processing an \cs{item} resets the
%   sub-level counter one nesting depth below the current level
%   (e.g.\ \texttt{numpropii} at level~1).  \texttt{reset=false} suppresses this behaviour, so that sub-item numbering continues from where it
%   left off across consecutive parent items. 
% \end{docKey}
%
% \begin{docKey}{crefname}{=\meta{type}}{no default}
%   When \textsf{cleveref} is loaded, assigns an arbitrary reference type to this proposition.  For example, \texttt{crefname=lemma} causes \cs{cref} to use the names defined by \cs{crefname}\texttt{\{lemma\}\{...\}\{...\}} instead of the default (private) \refEnv{prop} type.  The \meta{type} must be known to \textsf{cleveref}; new types can be declared with \cs{crefname}.
% \end{docKey}
%
% Four of the list-dimension keys documented in the next section---\refKey{labelwidth}, \refKey{labelsep}, \refKey{itemindent} and \refKey{labelindent}---may also be given to an individual \cs{item}, where they reposition the label of that item alone, overriding the value in force for the rest of the list.  (The other dimension keys have no effect at item level.)
% 
% \subsection{Keys for changing the list geometry}\label{sect:keys-dims}
%
% The keys in this section can be used in the following places: 
% \begin{itemize}
%   \item In the optional argument of \refEnv{prop}: the key applies to that environment only, not to any other \refEnv{prop} or \refEnv{inlineprop} environments that may be nested within it.  
%   \item In the argument of \refCom{propoptions}: the key 
% will apply to every subsequent \refEnv{prop} environment (in the current group), unless overridden by that environment's optional argument.
%   \item In the optional argument of |\usepackage{propositions}|: equivalent to \refCom{propoptions}.   
%   \item With \refCom{SetPropStyle} or \refCom{DeclareNumberedStyle}, to
% add the key to a given style.  
% \end{itemize}
% Five of the keys can also be used in the optional argument of |\item| to affect the geometry of that specific proposition (\refKey{align}, \refKey{labelwidth}, \refKey{labelsep}, \refKey{itemindent}, and \refKey{labelindent}).  The other keys will have no effect in an |\item| (or a \refCom{ptag}).  
% 
% \begin{docKey}{align}{\docKeyChoices{left,right,center,flush,nextline,flush-nextline}}{initially \docValue{left}}
%   How the label should be positioned.
%   \docValue{left} is the standard left-aligned label, its offset controlled by \refKey{labelwidth} and \refKey{labelsep};
%   \docValue{right} is right-aligned within the label box, like \texttt{enumerate};
%   \docValue{center} is centred within it;
%   \docValue{flush} aligns the label with the left margin of the item text;
%   \docValue{nextline} puts the label on a line of its own, and \docValue{flush-nextline} does both.
%   Has no effect inside \refEnv{inlineprop} or \refCom{ptag}.
% \end{docKey}
% 
% \begin{example}
% \begin{prop}
%   \item[L, align=left] Left aligned label.
%   \item[C, align=center] Center aligned label.
%   \item[R, align=right] Right aligned label.
%   \item[Long label, align=center] As in standard \LaTeX\ lists, 
%       longer labels expand to fill the label box and then push
%       the following text along to make room for themsselves.
%   \item[Flush label, align=flush] Flush aligned label.
%   \item[Sometimes a long label will deserve its own line,
%       align=nextline] Nextline aligned label.  
%   \item[Another rather long label,
%       align=flush-nextline] Flush-nextline aligned label.
% \end{prop}
% \end{example}
% 
% \begin{docKeys}[
%     doc parameter = {=\meta{length}},
%   ]
%   {
%     { doc name = topsep },
%     { doc name = partopsep },
%     { doc name = itemsep },
%     { doc name = parsep },
%     { doc name = leftmargin },
%     { doc name = rightmargin },
%     { doc name = labelwidth },
%     { doc name = labelsep },
%     { doc name = itemindent },
%     { doc name = listparindent },
%     { doc name = labelindent },
%   }
%   Override the standard \LaTeX{} list dimensions.  Accept the same values as \cs{setlength}, including rubber lengths (e.g.\ \texttt{itemsep=4pt plus 2pt}).
% 
% \refKey{labelindent} is not a standrd \LaTeX{} list dimension.  It positions the left edge of the label box at \meta{length} from the enclosing margin.  This introduces a redundancy: any one of \refKey{labelindent}, \cs{labelwidth}, \cs{leftmargin}, \cs{labelsep}, or \cs{itemindent} can be calculated from the four others, via the expression
% \[
% \refKey{labelindent} + \refKey{labelwidth} + \refKey{itemsep} = \refKey{leftmargin} + \refKey{itemindent}
% \]
% Whichever of these is not explicitly set will be computed from the ones that are explicitly set (or from the four most recently explicitly set) in such a way as to guarantee this identity.  Each dimension key also accepts the value~\texttt{*}, which means \emph{behave as if the key had not been set}: the dimension takes the document class's default, unless its value must shift to preserve the above identity.  This behaviour is identical to that of package \textsf{enumitem}.
%
% A dimension key can be set to any macro that expands to a dimension.  For example, one can set different dimensions for different nesting levels by using \refCom{proplevelchoice}:
% \begin{codebox}
% \propoptions{leftmargin = \proplevelchoice{2.5em, 0em, *}}
% \end{codebox}
% (Note that without the \texttt{*}, the last entry 0em would apply at every level below the second.)  
% \end{docKeys}
% 
% \begin{docKey}{tightspacing}{}{no value}
%   Sets all vertical spacing to the compact defaults that the standard document classes use for level-three lists (\refKey{topsep} and \refKey{itemsep} to \texttt{2pt} with stretch/shrink, \refKey{parsep} to \texttt{0pt}, \refKey{partopsep} to \texttt{1pt}).
% \end{docKey}
%
% \begin{docKey}{nosep}{}{no value}
%   Sets \cs{topsep}, \cs{itemsep}, and \cs{parsep} all to zero.
% \end{docKey}
%
% \begin{docCommand}{propformlabel}{}
%   Expands to the formatted label of the (approximately) \texttt{items}-th item in this
%   environment, computed at \verb|\begin{prop}| \emph{before} the list dimensions are applied,
%   so it can be used directly in dimension expressions.
%   It keeps that value for the whole environment: a dimension key is read
%   again for each item's label area, and a prediction that changed as the
%   list went along would size each item's label box to its predecessor's
%   label.
%   Typical use:
%   \begin{codebox}
%   \begin{prop}[items=20, 
%     leftmargin=\widthof{\propformlabel}+0.5em]
%   \end{codebox}
%   sizes the left margin to accommodate labels up to the 20th item.
% \end{docCommand}
%
% \begin{docCommand}{propwidestlabel}{}
%   The same as \refCom{propformlabel}, but with every digit replaced by the digit that makes the label widest (an~\texttt{8} in many fonts).  Using it in place of \refCom{propformlabel} in a dimension expression makes the dimension depend on how many digits the label has rather than on which digits they are, so that a run of numbered environments keeps a steady margin instead of shifting at every change of number.  (The substitution is used for measurement only; the labels themselves are untouched.)  (Used by the built-in \texttt{fitmargin} and \texttt{outerfit} styles.)
% \end{docCommand}
%
%
% \begin{docKey}{items}{=\meta{n}}{initially \texttt{1}}
%   Indicates that approximately \meta{n} items are expected in this environment.
%   The only effect of this key is in conjunction with \refCom{propformlabel}, to compute a preview label wide enough for the \meta{n}\/th expected item, so that dimension expressions such as
%   \texttt{leftmargin=\cs{widthof}\{\refCom{propformlabel}\}+0.5em} reserve enough space for the
%   widest label.  Has no effect on actual item processing or counter stepping.
% \end{docKey}
%
% \begin{docKey}{continue}{=\meta{boolean}}{initially \texttt{true}}
%   When a \refEnv{prop} environment with \texttt{continue=true} is immediately followed by another such environment, (with no intervening
%   paragraph text), the normal \cs{topsep}-based inter-list
%   space is replaced with \cs{itemsep}\,+\,\cs{parsep}, giving the visual
%   appearance of a single continuous list.
% \end{docKey}
%
% \subsection{Other environment-level keys}\label{sect:keys-env}
%
% The keys in this section have effect in both the \refEnv{prop} and \refEnv{inlineprop} environments.  They can also be used with \refCom{propoptions}, |\usepackage|, and \refCom{SetPropStyle}, just like the keys in the previous subsection.  
% 
% \begin{docKey}{named style}{=\meta{style}}{initially \texttt{proposition}}
%   The style when an |\item| or \refCom{ptag} has a value for \refKey{name} but no explicit \refKey{style}.
% \end{docKey}
%
% \begin{docKey}{named ptag style}{=\meta{style}}{initially empty}
%   If set, overrides \refKey{named style} for \refCom{ptag} items only.
% \end{docKey}
%
% \begin{docKey}{nameless style}{=\meta{style}}{initially \texttt{numbered}}
%   The style used when \cs{item} or \refCom{ptag} has no value for \refKey{name} and no explicit \refKey{style}.  A \refKey{counter} does not affect the choice: it says how the item is numbered, and this is the style meant to look right around a number.
% \end{docKey}
%
% \begin{docKey}{nameless ptag style}{=\meta{style}}{initially empty}
%   If set, overrides \refKey{nameless style} for \refCom{ptag} items only.
% \end{docKey}
% 
% The choice between them turns on \refKey{name} alone, read from the whole key
% list---\refCom{propoptions}, then the environment argument, then the item's
% own argument.  An item counts as named if a name reaches it from any of those,
% so \verb|\begin{prop}[name=foo]\item bar| gives the same result as
% \verb|\begin{prop}\item[name=foo] bar|.  An explicit \refKey{style} overrides
% the choice wherever it is set.
% 
% \begin{docKeys}[
%     doc parameter = {=\meta{code}},
%   ]
%   {
%     { doc name = wrapper begin },
%     { doc name = wrapper end },
%   }
%   Insert arbitrary \meta{code} immediately before the beginning and after the end of the environment, so that the whole list can (for example) be wrapped in another environment. 
% 
% Any value that contains a comma (such as a comma-separated list of options to an environment) must be enclosed in braces, so that the comma is not read as a key separator:
% \begin{example}
% \begin{prop}[
%   wrapper begin = {\begin{tcolorbox}[
%       colframe = red, colback = white]},
%   wrapper end   = {\end{tcolorbox}}]
%   \item[Red] A proposition in a red frame.
%   \item And a second one, in the same frame.
% \end{prop}
% \end{example}
% The wrapping environment must be one that can be split into separate begin and end
% code---that is, it must not read its body as a macro argument via \cs{collect@body} or similar.
% \end{docKeys}
%
% The following command is provided for use with \refKey{wrapper begin}:
% \begin{docCommand}{propoperativeleftmargin}{}
%   A read-only length giving the \refKey{leftmargin} a \refEnv{prop} environment (with no optional argument) would use, given the current defaults set by \refCom{propoptions} and the current nesting level.  It is recomputed at every \verb|\begin{prop}|, so it is valid inside a wrapper (before the
%   environment's own \refKey{leftmargin} has taken effect).  For example, the built-in \texttt{framed} style uses this command in the value of \refKey{wrapper begin} to make the margins of framed environments match those of regular environments.
% \end{docCommand}
%
% \subsection{Global key}
% \label{sect:keys-global}
%
% The following key can only be set in the optional argument of |\usepackage|, or in the preamble with \refCom{propoptions}.  
% \begin{docKey}{equations}{}{no value, \textbf{global only}}
%   Installs hooks so that the \LaTeX\ and \textsf{amstex} displayed equation environments (such as \texttt{equation} and \texttt{align}) use the same formatting as the special \texttt{equation} prop style.  The \texttt{equation} style's \refKey{display format} and \refKey{ref format} keys are used for generating equation numbers and cross-references to them.  
% 
% Redefining the \texttt{equation} style, e.g.~with
%\begin{codebox}
% \SetPropStyle{equation}{format = [#1]}
%\end{codebox}
%   will automatically update the hooks.
% 
% The \refKey{equations} key also sets \texttt{nameless style\,=\,eqnum}, so that top-level |\item|s with no name will also use the \texttt{equation} style, while lower-level |\item|s will use other kinds of numbering: for details, see \cref{sect:builtin-styles} below.  
% 
% \end{docKey}
%
% \section{Cross-referencing commands}\label{sect:xref}
%
% Labels placed after |\item| items (within \refEnv{prop}) work with the standard
% |\label|/|\ref| mechanism.  The key difference from ordinary
% \LaTeX{} references is that |\ref| produces \emph{formatted}
% output: for example, |\textbf| might be applied to the name, or the number might be wrapped in parentheses.  The formatting is controlled by the |format| key (or separately by |display format| and |ref format|).
%
% \begin{docCommands}{
%   { doc name = Ref,  doc parameter = \marg{label} },
%   { doc name = {Ref*}, doc parameter = \marg{label} },
% }
%   Titlecase variants of |\ref| and |\ref*|: uppercases the first letter of the
%   formatted output.  (For example, if |\ref{thesis}| produces
%   `the Identity Theory', then |\Ref{thesis}| produces
%   `The Identity Theory'.)  The starred form suppresses the hyperlink.
%   Note: |\Ref| only affects references produced by this package (which are stored
%   via \refCom{propapply}); for other references, it behaves like |\ref|.
% \end{docCommands}
%
% \begin{docCommands}{
%   { doc name = nref,  doc parameter = \marg{label} },
%   { doc name = {nref*}, doc parameter = \marg{label} },
%   { doc name = Nref,  doc parameter = \marg{label} },
%   { doc name = {Nref*}, doc parameter = \marg{label} },
% }
%   ``Naked ref.''  Outputs the bare reference content with all formatting stripped.  If \cs{ref}\texttt{\{premise\}} produces~`(P1)', then \cs{nref}\texttt{\{premise\}} produces~`P1'.  The starred form suppresses the hyperlink.  \cs{Nref} is the titlecase variant: it uppercases the first letter of the bare content.
% \end{docCommands}
%
% |\nref| can be useful in the argument of |\item|, when the
% the name of one proposition should depend on that of another:
% \begin{example}
% \SetPropStyle{proposition}{format=(\textbf{#1})}
% \begin{prop}
%   \item[Phys] Everything is physical. \label{phys2}
%   \item[\nref{phys2}*] Almost everything is physical.
%   \label{newphys2}
%   \item[\ref{phys2}*] This one has two sets of parentheses,
%   which is probably not desired!  Note that 
%   the previous proposition \ref{newphys2} avoided this by using
%   |\nref| in the optional argument
%    of |\item|.
% \end{prop}
% \end{example}
% 
% \emph{Warning:} documents where the name of one item includes
% a reference to that of another, and there are further 
% references to that item, will require multiple
% \LaTeX\ runs to resolve all references.  To save time, 
% it is better to avoid long chains of dependencies of this sort.
% 
% \begin{docCommands}{
%   { doc name = oref,  doc parameter = \oarg{prefix}\oarg{suffix}\marg{label} },
%   { doc name = {oref*}, doc parameter = \oarg{prefix}\oarg{suffix}\marg{label} },
%   { doc name = Oref,  doc parameter = \oarg{prefix}\oarg{suffix}\marg{label} },
%   { doc name = {Oref*}, doc parameter = \oarg{prefix}\oarg{suffix}\marg{label} },
% }
%   ``Ref with options.''  Extends \cs{ref} by injecting a prefix and/or suffix \emph{inside} the formatting.  With one optional argument, \meta{suffix} is appended; with two, \meta{prefix} is prepended and \meta{suffix} appended.  For instance, if \cs{ref}\texttt{\{premise\}} produces~`(P1)', then \cs{oref}\texttt{[*]\{premise\}} produces~`(P1*)' and \cs{oref}\texttt{[old\string~][*]\{premise\}} produces~`(old\string~P1*)'.  
% 
% \cs{Oref} is the titlecase variant; the starred forms suppress the hyperlink.
% \end{docCommands}
% 
% |\oref| can also be useful in the name of |\item|s, if
% one wants the display format for the modified item
% to depend on that originally used
% \begin{example}
% \begin{prop}
%   \item[style=plain, name=\oref[$^\dag$]{phys2}]
%   This will use boldface and parentheses because the
%   original referenced item did.
% \end{prop}
% \end{example}
% 
% Another handy use for |\oref| is in combination with |\nref| to refer to ranges:
% \begin{example}
% The first two numbered examples in this document
% were \oref[--\nref{atomism}]{atoms}.
% \end{example}
%
% 
% \begin{docCommands}{
%   { doc name = lastref,  doc parameter = \oarg{prefix}\marg{suffix} },
%   { doc name = Lastref,  doc parameter = \oarg{prefix}\marg{suffix} },
% }
%   Produces a reference (witth no hyperlink) to the most recently processed \cs{item} or \refCom{ptag}, even without a \cs{label}.  Useful for back-references in running text.  With one argument, \meta{suffix} is appended; with two, \meta{prefix} is also prepended.  Use \cs{lastref}\texttt{\{\}} for a plain reference.  \cs{Lastref} is the titlecase variant.
% \end{docCommands}
%
% \begin{docCommands}{
%   { doc name = nlastref, doc parameter = {} },
%   { doc name = nLastref, doc parameter = {} },
% }
%   Like \cs{lastref}\texttt{\{\}}, but returns the bare content without formatting.  \cs{nLastref} is the titlecase variant.
% \end{docCommands}
%
% \begin{docCommands}{
%   { doc name = parentref,  doc parameter = \oarg{prefix}\marg{suffix} },
%   { doc name = Parentref,  doc parameter = \oarg{prefix}\marg{suffix} },
% }
%   Inside a nested \refEnv{prop} (or \refEnv{inlineprop}), produces a formatted reference to the most recent item of the enclosing level.  Same argument convention as \refCom{lastref}.  \cs{Parentref} is the titlecase variant.
% \end{docCommands}
%
% \begin{docCommands}{
%   { doc name = nparentref, doc parameter = {} },
%   { doc name = nParentref, doc parameter = {} },
% }
%   Like \cs{parentref}\texttt{\{\}} but returns the bare content without formatting.  Takes no arguments; simply output any desired suffix directly afterwards.  \cs{nParentref} is the titlecase variant.  
% \end{docCommands}
%
% \refCom{parentref} and \refCom{nparentref} are useful for making subitems whose names derive from their parent's:
% \begin{example}
% \begin{prop}
%   \item[P1, ref format=(#1)] \label{claim}
%   \begin{prop}[counter format=\alph{#1}, 
%     display format=\textit{#1.}, ref format=\parentref{#1}]
%     \item \label{positive}
%     Some things are physical.
%     \item \label{negative}
%     Some things are not physical.
%   \end{prop}
% \end{prop}
% Of the two parts of \ref{claim}, \ref{positive} is far more controversial than \ref{negative}.  Thus, we will mostly be considering part \nref{negative}.  
% \end{example}
%
% Many of the built-in numbered styles use \refCom{parentref} in their \refKey{ref format}, to achieve this sort of composite effect.
%
% \subsection{How cross-referencing works}
%
% \begin{docCommand}{propapply}{\marg{template}\marg{content}}
%   Internally, each reference is stored in the \texttt{.aux} file as \cs{propapply}\marg{template}\marg{content}.  The \meta{template} contains formatting with the placeholder \refCom{propfmtarg} where content appears.  At reference time, \cs{propapply} evaluates the template with \refCom{propfmtarg} bound to \meta{content}.  The \refCom{oref} and \refCom{nref} commands work by locally redefining \cs{propapply}.
%
%   In normal use, you need not interact with \cs{propapply} directly.
% \end{docCommand}
%
% \begin{docCommand}{propfmtarg}{}
%   Placeholder used inside templates; expands to the content argument of the enclosing \refCom{propapply}.
% \end{docCommand} 
% 
% \section{Defining and modifying styles}\label{sect:styles}
%
% Styles, equivalent to bundles of key-value settings,
% can be defined, and used freely in the optional arguments of |\item|, \refCom{ptag}, \refEnv{prop}, \refEnv{inlineprop}, and the argument of \refCom{propoptions}.  
% Styles can freely be combined, and the definition of 
% one style can reference another (in which case redefining
% the latter style will change the effect of the former style.)
%  
% \begin{docCommand}{SetPropStyle}{\marg{name}\marg{keys}}
%   Defines or modifies a prop style for use with the \refKey{style} key.  All item-level keys (\autoref{sect:keys-item}) are accepted, plus the following:
% \end{docCommand}
%
% \begin{docKey}[][doc label=setpropstyle/style]{style}{=\meta{parent}}{no default}
%   Inherit from a parent style.  When an item is created, the parent's settings are loaded first (recursively, if the parent itself has a parent), then this style's own keys are applied on top.
%
%   The argument may be a macro which is expanded when the item is created: for example, a style with \texttt{style=}\cs{\proplevelchoice}\texttt{{\marg{style1},\marg{style2},\marg{style3}}} will resolve to \marg{style1}, \marg{style2}, \marg{style2} depending on the nesting depth.  The built-in \texttt{numbered} and \texttt{eqnum} styles use this mechanism.
% \end{docKey}
%
% \begin{docKey}{macro}{=\meta{command}}{no default}
%   A new user macro, equivalent to \cs{item}\texttt{[style=}\meta{name}\texttt{]}.  Any further keys given to the macro are passed to \cs{item}.
% \end{docKey}
%
% If the style \meta{name} already exists, \refCom{SetPropStyle} modifies or adds keys.  For example, |\SetPropStyle{proposition}{align=flush}| changes the alignment of the built-in |proposition| style while preserving its other settings.
%
%
% \begin{example}
% \SetPropStyle{angle}{
%   labelindent    = 0em,
%   display format = \textbf{$\langle$#1$\rangle$},
%   ref format     = $\langle$#1$\rangle$,
%   macro          = \angitem
% }
% \begin{prop}
%   \angitem[Angle thesis] Everything is angular.
% \end{prop}
% No further discussion of \lastref{} is needed.
% \end{example}
%
% \begin{docCommand}{DeclareNumberedStyle}{\marg{name}\oarg{keys}}
%   Creates a new \LaTeX{} counter named \meta{name} and a matching prop style with \texttt{counter=}\meta{name}.  All \refCom{SetPropStyle} keys are accepted, plus:
% \end{docCommand}
%
% \begin{docKey}{parent}{=\meta{counter}}{no default}
%   A parent counter; the new counter resets when the parent steps (same mechanism as \cs{numberwithin}).  A dedicated \texttt{prop} counter (stepped by each \refEnv{prop} and \refEnv{inlineprop}) is available for non-persistent numbering.
% \end{docKey}
%
% \begin{example}
% \DeclareNumberedStyle{P}
% \begin{prop}
%   \item[counter=P] First premise. \label{p1}
%   \item[counter=P] Second premise. \label{p2}
% \end{prop}
% From \ref{p1} and \ref{p2}\ldots
% \end{example}
%  
% \section{Built-in styles}\label{sect:builtin-styles}
%
% The following prop styles are predefined.
% Each entry shows the defining code (using user-facing commands),
% and each group of styles ends with a live example.
% All styles can be modified with \refCom{SetPropStyle}; the definitions are reproduced here to facilitate modification.
%
% \subsubsection*{Text styles}
% 
% \begin{description}
% \item[\texttt{plain}] Unformatted text label.
% \begin{codebox}
% \SetPropStyle{plain}{format = #1}
% \end{codebox}
%
% \item[\texttt{proposition}] The standard style assigned to named propositions.  By default, uses boldface for both the label and references.  
% \begin{codebox}
% \SetPropStyle{proposition}{format = \textbf{#1}}
% \end{codebox}
%
% \item[\texttt{thesis}] Intended for named propositions with a longer name.  The name begins at the text margin (\texttt{flush} alignment), and is set in small caps; references use plain font.
% \begin{codebox}
% \SetPropStyle{thesis}{display format = \textsc{#1},
%   ref format=#1, align = flush}
% \end{codebox}
%
% \item[\texttt{vignette}] Intended for things like example vignettes and comments.  Italic name at the text margin, and italic references, separated from the text by a colon.
% \begin{codebox}
% \SetPropStyle{vignette}{ref format = \textit{#1},
%   align = flush, label format = \textit{#1:}}
% \end{codebox}
%
% \item[\texttt{bullet}] Bullet symbol varying by depth (like |\itemize|).
% \begin{codebox}
% \SetPropStyle{bullet}{align = center,
%   name = \proplevelchoice{\textbullet,
%     {\normalfont\textendash}, \textasteriskcentered,
%     \textperiodcentered},
%   display format = #1}
% \end{codebox}
% \end{description}
%
% \begin{example}
% \begin{prop}
%   \item[One, style=plain] \label{bs:plain}
%   A proposition in style |plain|, cited as \ref{bs:plain}.
%   \item[Two, style=proposition] \label{bs:prop}
%   A proposition in style |proposition|, cited as \ref{bs:prop}.
%   \item[Three, style=thesis] \label{bs:thesis}
%   A proposition in style |thesis|, cited as \ref{bs:thesis}.
%   \item[Four, style=vignette] \label{bs:vignette}
%   A proposition in style |vignette|, cited as \ref{bs:vignette}.
%   \item[style=bullet] \label{bs:bullet}
%   A proposition in style |bullet|, cited as \ref{bs:bullet}---though
%   it is not often that one would want to cite an item in this style.
% \end{prop}
% \end{example}
% 
% \subsubsection*{Numbered styles}
% 
% \begin{description}
% \item[\texttt{numbered}] The default nameless style.  Selects one of 
%    the helper styles \texttt{levelone}--\texttt{levelfive}, depending
%    on nesting depth.    
% \begin{codebox}
% \SetPropStyle{levelone}{counter = numpropi, format = (#1)}
% \SetPropStyle{leveltwo}{counter = numpropii,
%   display format = #1., ref format = \parentref{#1}}
% \SetPropStyle{levelthree}{counter = numpropiii,
%   display format = (#1), ref format = \parentref{.#1}}
% \SetPropStyle{levelfour}{counter = numpropiv,
%   display format = #1., ref format = \parentref{#1}}
% \SetPropStyle{levelfive}{counter = numpropv,
%   display format = (#1), ref format = \parentref{.#1}}
% \SetPropStyle{numbered}{style = \proplevelchoice{
%   levelone, leveltwo, levelthree, levelfour, levelfive}}
% \end{codebox}
% 
% \item[\texttt{equation}] Uses the |equation| counter.  Note that this style has a special behavior when the |equations| option is active: changing its \refKey{display format} and \refKey{ref format} keys (or both, by setting \refKey{format}) will also change the corresponding hooks used to create the tags for numbered equations make the \texttt{equation} environment and \textsf{amstex} environments like \texttt{gather}.
% \begin{codebox}
% \SetPropStyle{equation}{counter = equation, format = (#1)}
% \end{codebox}
% \end{description}
%
% \begin{description}
% \item[\texttt{eqnum}] Like |numbered|, but uses |equation| instead 
% of |levelone| at the outer level.  The |equations| package option sets
% |default nameless style = eqnum|.  Since this manual uses this option,
% its outer-level nameless items use the |equation| style.
% \begin{codebox}
% \SetPropStyle{eqnum}{style = \proplevelchoice{
%   equation, leveltwo, levelthree, levelfour, levelfive}}
% \end{codebox}
% \end{description}
% 
% \begin{example}
% \begin{prop}
%   \item \label{outer}
%   This is an outermost numbered item.  Since the default style for
%   nameless items is |eqnum|, it uses the |equation| style.
%   \begin{prop}
%     \item \label{second}
%     This is a second level item, using |leveltwo|.
%     \begin{prop}
%       \item \label{third}
%       This is a third level item, using |levelthree|.
%       \begin{prop}
%         \item \label{fourth}
%         This is a fourth level item, using |levelfour|.
%         \begin{prop}
%           \item \label{fifth}
%           This is a fifth level item, using |levelfive|.
%         \end{prop}
%         \item Another fourth level item.
%       \end{prop}
%       \item Another third level item.
%     \end{prop}
%     \item Another second level item.
%   \end{prop}
% \end{prop}
% We hope you enjoyed reading \ref{outer}, \ref{second}, \ref{third},
% \ref{fourth}, and \ref{fifth}. 
% \end{example}
% 
% \begin{description}
% \item[\texttt{roman}] Roman numerals.  At the
% outer level, they use their own counter (reset every section); inside 
% nested lists, they use the counter appropriate to the nesting
% level, so one can easily make roman-numbered sublists.
% \begin{codebox}
% \DeclareNumberedStyle{roman}[parent = section,
%   counter format = \roman{#1}, format = (#1)]
% \SetPropStyle{roman}{counter = \proplevelchoice{
%   roman, numpropii, numpropiii, numpropiv, numpropv}}
% \end{codebox}
%
% \item[\texttt{alph}] Letters.  Works the same as |roman|, but with 
% letters.  Uses its own dedicated counter at the outer level.  
% \begin{codebox}
% \DeclareNumberedStyle{alph}[parent = section,
%   counter format = \alph{#1}, display format=#1., 
%   ref format = (#1)]
% \SetPropStyle{alph}{counter = \proplevelchoice{
%   alph, numpropii, numpropiii, numpropiv, numpropv}}
% \end{codebox}
%
% \begin{example}
% \begin{prop}
%   \item[Basic classification, ref format={the \textit{#1}}] 
%   There are three kinds of people. \label{complex}
%   \begin{prop}
%     \item[style=roman] \label{partone} Those who know how to count, 
%     comprising in turn:
%     \begin{prop}
%       \item[style=alph] \label{parta} Those who know how to count up to 
%    some number, but not beyond.
%       \item[style=alph] \label{partb} Those who can keep going indefinitely.
%     \end{prop}
%     \item[style=roman] \label{parttwo} Those who do not know how to count.
%   \end{prop}
% \end{prop}
% For \ref{complex} to serve its purpose, both \ref{partone} (and 
% its two components \ref{parta} and \ref{partb}) and 
% \ref{parttwo} are needed.  
% \begin{prop}
%   \item[style=roman]
%   The |roman| and |alph| styles are also useful for creating ad-hoc 
%   numbered lists at the outer level.  
%   \item[style=roman]
%   Like this one.  
% \end{prop}
% \end{example}
% 
% \item[\texttt{hierarchical}] Produces 1, 1.1, 1.1.1\,\ldots\ numbering.  Defined via two helper styles:
% \begin{codebox}
% \SetPropStyle{h-base}{counter = numpropi,
%   counter format = \arabic{#1}, ref format = #1, 
%   display format = #1.}
% \SetPropStyle{h-sub}{
%   counter = \proplevelchoice{numpropi, numpropii,
%     numpropiii, numpropiv, numpropv},
%   counter format = \arabic{#1},
%   format = \parentref{.#1}}
% \SetPropStyle{hierarchical}{style = \proplevelchoice{
%   h-base, h-sub}, tightspacing}
% \end{codebox}
% \end{description} 
% 
% Note that since the optional arguments of \refEnv{prop} and \refEnv{inlineprop} only affect the |\item|s in the \emph{immediate} scope of that environment (not of any nested environments), styles like |hierarchical|, which one presumably wants to apply to apply an environment along with all its sub-environements, sub-sub-environments, etc., will need to be set using \refCom{propoptions}.  (The scope of \refCom*{propoptions} can be controlled by creating a \TeX{} group.)
% 
% \begin{example}
% \begingroup
% \propoptions{style = hierarchical, leftmargin=3em, labelindent=0em}
% \begin{prop}
%   \item \label{theworld} The world is everything that is the case.
%   \begin{prop}
%     \item \label{totality}
%     The world is the totality of facts, not of things.
%     \begin{prop}
%       \item 
%       The world is determined by the facts, and by their being all the
%       facts.
%       \item
%       For the totality of facts determines what is the case, and also 
%       whatever is not the case.
%     \end{prop}
%   \end{prop}
% \end{prop}
% Proposition \ref{totality} helps elucidate the meaning of 
% proposition \ref{theworld}.  
% \endgroup
% \end{example}
%
%
% \subsubsection*{Environment-level styles}
%
% These styles are designed to be used in 
% the optional argument of \refEnv{prop} or \refEnv{inlineprop}.
% 
% \begin{description}
% \item[\texttt{fitmargin}] Fits the left margin to the predicted width of the 
% label (computed using \refCom{propwidestlabel}), so that the label will never
% extend past the left margin of the following text. 
% \begin{codebox}
% \SetPropStyle{fitmargin}{
%   labelindent = 0pt,
%   leftmargin  = \widthof{\propwidestlabel} + \labelsep}
% \end{codebox}
%  (Explanation: \refCom{propwidestlabel} computes the widest label the environment's items are  expected to produce.  By setting \refKey{labelindent} to zero, we make sure that the \refKey{labelwidth} will be sized to fit the computed \refKey{leftmargin}.)  
% 
% When a list will contain several numbered items, you can use the \refKey{items} key to tell the environment how many |\item|s it contains, so that it can properly anticipate how wide the widest label will be.
% \end{description}
%
% \begin{example}
% \begin{prop}[name=Fitted Margin, style=fitmargin]
%   \item Notice that the |name| key needs to be set in the optional 
%   argument of |prop| rather than |item|, so that the style knows 
%   how much space needs to be reserved.
% \end{prop}
% \begin{prop}[items=2, style=fitmargin]
%   \item
%   The use of |items=2| is crucial here; without it, we would
%   only reserve enough space for a one-digit number.
%   \item 
%   This happens to be where the |equation| counter hits value 10.
% \end{prop}
% The |hierarchical| style arguably looks better combined with |fitmargin|:
% \begingroup
% \propoptions{style=hierarchical, style=fitmargin}
% \begin{prop}
%   \item What is the case---a fact---is the existence of states of affairs.
%   \begin{prop}
%     \item A state of affairs (a state of things) is a combination
%     of objects (things).
%     \begin{prop} 
%       \item 
%       It is essential to things that they should be possible 
%       constituents of states of affairs.
%       \item
%       In logic nothing is accidental: if a thing can occur in a 
%       state of affairs, the possibility of the state of affairs 
%       must be written into the thing itself.
%     \end{prop}
%   \end{prop}
% \end{prop}
% \endgroup
% \end{example}
% 
% \begin{description}
% \item[\texttt{outerfit}] 
% This style behaves similar to \texttt{fitmargin} at the outer nesting level (with a bit more space between label and text), but does nothing at other levels.  Intended to be set once using \refCom{propoptions}, for a document that wants `fitmargin'-like behavior for its top-level propositions, but not for lower-level propositions (where adjusting to acommodate, e.g., roman numerals of different lengths would be a delicate task).  
% 
% This matches the behaviour of the |\ex.| command in package 
% \textsc{linguex}, widely used in linguistics.  
% 
% \begin{codebox}
% \SetPropStyle{outerfit}{
%   labelindent = \proplevelchoice{0pt, *},
%   leftmargin  = \proplevelchoice{
%     \widthof{\propwidestlabel} + 1.3em, *}}
% \end{codebox}
%   (Note the use of \texttt{*} in the argument of \refCom{proplevelchoice}, which leaves the deeper levels as though neither key had been set.)
% \end{description}
% 
% \begin{description}
% \item[\texttt{framed}] Puts an outline around a list (requires the \textsf{tcolorbox}
%   package to be loaded).  Change the
%   padding with \verb|\setlength\propframepad{...}|.
% \begin{codebox}
% \SetPropStyle{framed}{
%   align = flush, leftmargin = 0pt, rightmargin = 0pt,
%   labelindent = {}, continue = false,
%   wrapper begin = {\begin{tcolorbox}[
%       colback = white, colframe = black,
%       boxrule = 0.4pt, arc = 0pt, boxsep = 0pt,
%       left skip  =
%         \dimexpr\propoperativeleftmargin-\propframepad\relax,
%       right skip =
%         \dimexpr\propoperativeleftmargin-\propframepad\relax,
%       left = \propframepad, right = \propframepad,
%       top  = \propframepad, bottom = \propframepad]},
%   wrapper end = {\end{tcolorbox}},
% }
% \end{codebox}
%  (Explanation: \texttt{leftmargin\,=\,0} means that the left margin \emph{inside} the frame is zero.  But the use of 
%   \refCom{propoperativeleftmargin} indents the whole \texttt{tcolorbox} environment by the right amount for the  the
% left margin of the enclosed material to appear at the same position that would have been used for a list without the \texttt{frame} style, with the frame rule one
%   \cs{propframepad} further out.)
%
% \begin{example}
% \begin{prop}[style=framed]
%   \item[Important Claim]
%   This claim is so important that it deserves to 
%   put in a special box!
% \end{prop}
% \end{example}
%
% \item[\texttt{standard}] 
% A style that resets all the environment-level keys back to their default value.  (This is useful, since there is otherwise no easy way to `unset' a globally-set style.)  Item-level keys like \refKey{align} and \refKey{display format} are not affected, so these will still be set by the the operative \refKey{named style} or \refKey{nameless style} defaults.  (To reset \refKey*{align} along with the other keys, just set \verb|[style=standard, align=left]|.)
% \end{description}
%
%
% \section{Compatibility}
%
% The \textsf{propositions} package is designed to work with \textsf{hyperref}, \textsf{cleveref}, \textsf{amsmath}, and \textsf{tcolorbox}.
% \begin{itemize}
%    \item 
%    \textsf{amsmath} is required for \refCom{ptag} and the |equations| option.  
%    \item 
%    With \textsf{hyperref} loaded, all cross-referencing 
%    commands generate hyperlinks, as usual.  
%    \item
%    With \textsf{cleveref} loaded, all proposition items are assigned to a private |prop| ``reference type'', which by default has no special name, so |\cref| and |\ref| will generate the same output.  The |crefname| key can override this.  
%    \item 
%    The built-in \texttt{framed} style requires \textsf{tcolorbox} to be loaded.
% \end{itemize}
% None of these packages has to be loaded in any particular order relative to
% \textsf{propositions}: each is detected either at load time or at
% \verb|\begin{document}|, whichever is needed.  The usual external conventions
% still apply---\textsf{hyperref} late, and \textsf{cleveref} after
% \textsf{hyperref}---which gives:
% \begin{Verbatim}[gobble=2]
% \usepackage{amsmath}      % if using \ptag or the equations option
% \usepackage{tcolorbox}    % if using the framed style
% \usepackage{hyperref}
% \usepackage{propositions}
% \usepackage{cleveref}     % if used
% \end{Verbatim}
%
% \section{Known issues}
%
% When using \refCom{ptag} with a named counter (e.g.\ |\ptag[counter=P]|)
% inside an \textsf{amsmath} equation environment, \textsf{hyperref}
% may emit warnings of the form:
% \begin{Verbatim}[gobble=2]
% pdfTeX warning: destination with the same
% identifier (name{equation.N}) has been already
% used, duplicate ignored
% \end{Verbatim}
% These warnings are harmless and do not affect the correctness
% of cross-references.
%
% \section{Release notes}
%
% \begin{description}
% \item[0.9] Initial public release.
% \end{description}
%
% \StopEventually{}
%
% \section{Implementation}
%
%    \begin{macrocode}
%<*package>
% propositions.sty --- A flexible system for labelling and cross-referencing displayed propositions.
\ProvidesExplPackage {propositions} {2026/08/02} {0.9}
  {Proposition labeling with key-value interface}

\RequirePackage { calc }

% ====================================================================
% Internal variables
% ====================================================================

% --- Nesting level ---
\int_new:N  \g__props_level_int

% --- Per-item state (set during \item / \ptag processing) ---
% These are cleared at the start of \__props_resolve_item:n and then
% populated by key parsing and style loading.  Emptiness of a tl
% indicates the key was not set (no separate boolean tracking needed).
\tl_new:N   \l__props_name_tl
\tl_new:N   \l__props_style_tl
\tl_new:N   \l__props_counter_tl
\tl_new:N   \l__props_alignment_tl
\tl_new:N   \l__props_pi_labelwidth_tl
\tl_new:N   \l__props_pi_labelsep_tl
\tl_new:N   \l__props_pi_itemindent_tl
\tl_new:N   \l__props_pi_labelindent_tl
\dim_new:N  \l__props_save_labelwidth_dim
\dim_new:N  \l__props_save_labelsep_dim
\dim_new:N  \l__props_save_itemindent_dim
\tl_new:N   \l__props_ref_tl
\tl_new:N   \l__props_label_tl
\tl_new:N   \l__props_shorthand_tl
\tl_new:N   \l__props_gloss_tl

% Format functions (one-argument macros set by keys / style loading).
% These always have a definition (defaulting to identity or a standard format),
% so unlike the tl variables above, their "was set" status cannot be inferred
% from their value.
\cs_new:Npn \l__props_displayfmt:n     #1 { #1 }
\cs_new:Npn \l__props_reffmt:n      #1 { #1 }
\cs_new:Npn \l__props_shorthandfmt:n #1 { ~ [#1] }
\cs_new:Npn \l__props_glossfmt:n    #1 { ~ (#1) }
\cs_new:Npn \l__props_labelfmt:n    #1 { #1 }
\cs_new:Npn \l__props_counterfmt:n  #1 { }  %% empty = not set
\bool_new:N \l__props_has_counter_format_bool

% --- Environment mode ---
% True inside a prop environment, false inside inlineprop.
% Controls whether \item outputs a display label or inline text.
\bool_new:N \g__props_display_mode_bool

% --- Global settings ---
\tl_new:N   \l__props_named_style_tl             %% default style for named items
\tl_new:N   \l__props_named_ptag_style_tl        %% ptag override for named items; empty = fall back
\tl_new:N   \l__props_nameless_style_tl          %% default style for nameless items
\tl_new:N   \l__props_nameless_ptag_style_tl     %% ptag override for nameless; empty = fall back
\bool_new:N \g__props_equations_bool         %% true if equations package option is set
\bool_new:N \g__props_eqhooks_bool           %% true if equation format hooks should be installed
\cs_new:Npn \__props_eqdispfmt:n #1 { (#1) } %% display format for equation tags
\cs_new:Npn \__props_eqreffmt:n  #1 { (#1) } %% ref format for equation labels

% --- Working variables ---
\tl_new:N   \l__props_display_text_tl    %% what appears in the document
\tl_new:N   \l__props_ref_text_tl        %% what goes into \@currentlabel
\tl_new:N   \l__props_item_output_tl     %% formatted display (displayfmt + shorthand + gloss)
\tl_new:N   \l__props_item_arg_tl        %% per-item argument, bare name normalised to name={...}
\tl_new:N   \l__props_keylist_tl        %% the three default layers plus the item argument, assembled
\bool_new:N \l__props_valueless_key_bool %% true when an entry of that argument is a key given without a value
\bool_new:N \l__props_ptag_bool          %% true during \ptag processing
\bool_new:N \l__props_nextline_bool     %% true when an align=nextline label has already started the body
\bool_new:N \l__props_counter_stepped_bool %% true if this item stepped its counter
\bool_new:N \l__props_titlecase_bool    %% true when \Ref etc. want titlecasing
\bool_new:N \l__props_reset_bool        %% true (default) = reset sub-level counter on \item
\bool_new:N \l__props_pi_any_bool       %% true if any per-item dimension is set for this item
%% Two layers of item-level defaults.  The cascading layer (\l__props_defaults_tl)
%% is fed by \propoptions and is inherited by nested environments; the env-local
%% layer (\l__props_env_defaults_tl) is fed by a prop's own optional argument and
%% is reset at the start of every environment, so an argument styles only that
%% environment's items, not those of any sub-environment.  \l__props_env_arg_bool
%% routes keys to the right layer (true while a prop argument is being read).
\tl_new:N  \l__props_defaults_tl
\tl_new:N  \l__props_env_defaults_tl
\bool_new:N \l__props_env_arg_bool
\bool_new:N \l__props_loading_defaults_bool %% true during the single processing pass so style= loads immediately
\int_new:N \l__props_env_items_int      %% items=n key (default 1; used by preview computation)
\int_set:Nn \l__props_env_items_int { 1 }
\tl_new:N  \g__props_env_preview_label_tl %% preview label built at env open for \propformlabel

% --- Parent-ref stacks and last-item storage ---
% Two global seq stacks hold the template/content of the parent item.
% Pushed on \begin{prop}/\begin{inlineprop}, popped on \end.
% Two global tl variables hold the most recent item's template/content,
% used by \lastref/\nLastref for linguex-style back-references.
\seq_new:N \g__props_parent_tpl_seq
\seq_new:N \g__props_parent_cnt_seq
\tl_new:N  \g__props_last_tpl_tl
\tl_new:N  \g__props_last_cnt_tl

% --- Anchor counter for hyperref ---
\newcounter { prop@anchor }
% Make hyperref destinations deterministic (not dependent on Hy@linkcounter,
% which amsmath does not save/restore between measuring and output passes).
% Note: hyperref prepends "prop@anchor." automatically in \H@refstepcounter,
% so \theHprop@anchor only needs the unique suffix.
\def \theHprop@anchor { \the\value{prop@anchor} }

% --- Prop environment counter ---
% Stepped by each \begin{prop} / \begin{inlineprop}.  Not displayed;
% exists solely so that \numberwithin{equation}{prop} can reset the
% equation counter per prop block if desired.
\newcounter { prop }

% ====================================================================
% \propapply — format/content separation for cross-references
% ====================================================================
%
% \propfmtarg is a protected placeholder.  In the aux file, format
% templates contain \propfmtarg where the content should go.
% \propapply{<template>}{<content>} evaluates the template with
% \propfmtarg set (via \protected@edef) to the content.  The
% \protected@edef expands expandable macros (including \propfmtarg
% tokens from an outer \propapply scope) while preserving robust
% commands like \textbullet.  This enables correct resolution of
% nested \parentref references.  \oref and \nref work by locally
% redefining \propapply to inject prefixes/suffixes or strip
% formatting.
%
% When hyperref is loaded, \propapply locally disables hyperref's
% link commands to suppress nested hyperlinks.  This matters because
% ref texts stored in the aux file may contain \ref, \oref, etc.;
% when \ref{item} renders the stored \propapply{template}{content},
% the entire output is already inside a hyperlink created by \ref,
% so any link-generating commands inside must be suppressed.
% (We avoid \NoHyper/\endNoHyper because they use \global
% assignments that break when \propapply is nested.)

\cs_new_protected:Npn \propfmtarg { }

\cs_new_protected:Npn \propapply #1#2
  {
    \group_begin:
    \bool_if:NTF \l__props_titlecase_bool
      {
        %% \protected@edef strips the e-TeX \protected flag from
        %% \propfmtarg, so subsequent inner calls can expand it.
        \protected@edef \propfmtarg { #2 }
        %% If the template starts with \propapply (nested ref via
        %% \parentref), run the normal path but keep the flag set
        %% so the inner \propapply applies ucfirst.  Otherwise,
        %% expand the template (substituting \propfmtarg) and apply
        %% \text_titlecase_first:n here.
        \tl_if_head_eq_meaning:nNTF { #1 } \propapply
          { #1 }
          {
            \bool_set_false:N \l__props_titlecase_bool
            \protected@edef \l_tmpa_tl { #1 }
            \exp_args:NV \text_titlecase_first:n \l_tmpa_tl
          }
      }
      {
        \protected@edef \propfmtarg { #2 }
        #1
      }
    \group_end:
  }

% ====================================================================
% \parentref / \nParentref / \lastref / \nLastref
% ====================================================================
%
% \parentref reads the top of the parent stacks, wrapping the result
% in \propapply so the parent's template is preserved.  When \nref
% strips the outermost \propapply, the parent contribution vanishes,
% leaving only the child content — as expected.
%
% \nParentref returns just the parent's content (bare, no template),
% suitable for use in \the<counter> definitions where the parent
% prefix should be part of the counter *name* and survive \nref.
%
% \lastref / \nLastref are analogous but read from the last-item
% globals instead of the parent stacks, enabling linguex-style
% back-references without \label.
%
% All four commands are expandable, so they resolve correctly
% inside \protected@edef (e.g. when building aux-file content).
%
% Argument convention:
%   \parentref{suffix}           — appends suffix to parent content
%   \parentref[prefix]{suffix}   — wraps parent content with both
%   \parentref{}                 — plain parent ref (empty suffix)
%
% Note: the last argument must be mandatory for expandable commands
% (xparse requirement), so the suffix is mandatory rather than optional.

\NewExpandableDocumentCommand \parentref { o m }
  {
    \IfValueTF { #1 }
      {
        \propapply
          { \seq_item:Nn \g__props_parent_tpl_seq { 1 } }
          { #1 \seq_item:Nn \g__props_parent_cnt_seq { 1 } #2 }
      }
      {
        \propapply
          { \seq_item:Nn \g__props_parent_tpl_seq { 1 } }
          { \seq_item:Nn \g__props_parent_cnt_seq { 1 } #2 }
      }
  }

\NewExpandableDocumentCommand \nparentref { }
  { \seq_item:Nn \g__props_parent_cnt_seq { 1 } }

\NewExpandableDocumentCommand \lastref { o m }
  {
    \IfValueTF { #1 }
      {
        \propapply
          { \g__props_last_tpl_tl }
          { #1 \g__props_last_cnt_tl #2 }
      }
      {
        \propapply
          { \g__props_last_tpl_tl }
          { \g__props_last_cnt_tl #2 }
      }
  }

\NewExpandableDocumentCommand \nlastref { }
  { \g__props_last_cnt_tl }

% ====================================================================
% \Parentref / \Lastref — titlecase versions (for running text)
% ====================================================================

\NewDocumentCommand \Parentref { o m }
  {
    \group_begin:
    \bool_set_true:N \l__props_titlecase_bool
    \IfValueTF { #1 }
      { \parentref [ #1 ] { #2 } }
      { \parentref { #2 } }
    \group_end:
  }

\NewDocumentCommand \Lastref { o m }
  {
    \group_begin:
    \bool_set_true:N \l__props_titlecase_bool
    \IfValueTF { #1 }
      { \lastref [ #1 ] { #2 } }
      { \lastref { #2 } }
    \group_end:
  }

% Titlecase variants of \cs{nparentref} and \cs{nlastref}.
\NewDocumentCommand \nParentref { }
  { \text_titlecase_first:n { \nparentref } }

\NewDocumentCommand \nLastref { }
  { \text_titlecase_first:n { \nlastref } }

% ====================================================================
% Variant generation
% ====================================================================

\cs_generate_variant:Nn \tl_gset_eq:NN { cN }
\cs_generate_variant:Nn \cs_gset_eq:NN { cN }
\cs_generate_variant:Nn \cs_set_eq:NN  { Nc }
\cs_generate_variant:Nn \seq_gpush:Nn  { NV }

% ====================================================================
% Style preset storage (live-parent model)
% ====================================================================
% For each declared style \meta{S}, we store two token lists:
%   \cs{g__props_style_\meta{S}_parent_tl}   — parent style expression
%     (possibly containing \cs{proplevelchoice}; empty = no parent)
%   \cs{g__props_style_\meta{S}_overrides_tl} — raw key-value pairs
%     (the settings from \cs{SetPropStyle}, minus \texttt{style=}
%     and \texttt{macro=})
%
% At resolution time, the parent chain is walked recursively:
% the innermost parent's overrides are applied first,
% then each outer style's overrides on top.

\seq_new:N \l__props_style_stack_seq   %% recursion stack for style loading

\cs_new_protected:Nn \__props_style_ensure:n
  {
    \tl_if_exist:cF { g__props_style_ #1 _parent_tl }
      {
        \tl_new:c { g__props_style_ #1 _parent_tl }
        \tl_new:c { g__props_style_ #1 _overrides_tl }
      }
  }

% Load a style's preset into the local item variables.
% If the style has a parent, the parent is loaded first (recursively),
% then this style's overrides are applied on top.
\cs_new_protected:Nn \__props_style_load:
  {
    \tl_if_exist:cTF { g__props_style_ \l__props_style_tl _parent_tl }
      {
        %% Save this style's name on the stack (recursive calls clobber it).
        \seq_push:NV \l__props_style_stack_seq \l__props_style_tl
        %% Load parent chain first (if any).
        \tl_if_empty:cF { g__props_style_ \l__props_style_tl _parent_tl }
          {
            \tl_set_eq:Nc \l__props_style_tl
              { g__props_style_ \l__props_style_tl _parent_tl }
            %% x-expand resolves \proplevelchoice at the current level.
            \tl_set:Nx \l__props_style_tl { \l__props_style_tl }
            \__props_style_load:
          }
        %% Restore this style's name and apply its overrides.
        \seq_pop:NN \l__props_style_stack_seq \l__props_style_tl
        \tl_set_eq:Nc \l_tmpa_tl
          { g__props_style_ \l__props_style_tl _overrides_tl }
        \tl_if_empty:NF \l_tmpa_tl
          { \exp_args:NnV \keys_set:nn { props / declare-style } \l_tmpa_tl }
      }
      {
        \msg_error:nnx { props } { unknown-style } { \l__props_style_tl }
      }
  }

\msg_new:nnn { props } { unknown-style }
  { Unknown~ prop~ style~ '#1'. }
\msg_new:nnn { props } { unknown-counter }
  { Counter~ '#1'~ not~ defined.~
    Use~ \token_to_str:N \DeclareNumberedStyle \{ #1 \} ~ in~ preamble. }
\msg_new:nnn { props } { item-in-math }
  { Proposition~ items~ cannot~ be~ used~ in~ math~ mode.~
    Use~ \token_to_str:N \ptag \ instead. }
\msg_new:nnn { props } { global-only-keys }
  { Key(s)~ '#1'~ ignored~ in~ prop~ optional~ argument~
    (use~ \token_to_str:N \propoptions \ instead). }

% ====================================================================
% l3keys: keys for \SetPropStyle / style application at item level
% ====================================================================
% Applied by \__props_style_load: when resolving an item.
% Keys that are global-only (list dimensions, tightspacing, etc.)
% are silently ignored via the unknown handler when a style is
% applied at item level; they take effect only via props/global.

\keys_define:nn { props / declare-style }
  {
    name            .tl_set:N  = \l__props_name_tl ,
    align           .tl_set:N  = \l__props_alignment_tl ,
    labelwidth      .tl_set:N  = \l__props_pi_labelwidth_tl ,
    labelsep        .tl_set:N  = \l__props_pi_labelsep_tl ,
    itemindent      .tl_set:N  = \l__props_pi_itemindent_tl ,
    labelindent     .tl_set:N  = \l__props_pi_labelindent_tl ,
    counter         .tl_set:N  = \l__props_counter_tl ,
    counter~format  .code:n    =
      {
        \bool_set_true:N \l__props_has_counter_format_bool
        \cs_set:Npn \l__props_counterfmt:n ##1 { #1 }
      } ,
    ref             .tl_set:N  = \l__props_ref_tl ,
    name~format     .cs_set:Np = \l__props_displayfmt:n #1 ,
    display~format  .cs_set:Np = \l__props_displayfmt:n #1 ,
    label~format    .cs_set:Np = \l__props_labelfmt:n #1 ,
    ref~format      .cs_set:Np = \l__props_reffmt:n #1 ,
    format          .code:n    =
      {
        \cs_set:Npn \l__props_displayfmt:n ##1 { #1 }
        \cs_set:Npn \l__props_reffmt:n ##1 { #1 }
      } ,
    ref~append      .code:n    =
      { \cs_set:Npn \l__props_reffmt:n ##1 { \parentref{#1} } } ,
    shorthand       .tl_set:N  = \l__props_shorthand_tl ,
    shorthand~format .cs_set:Np = \l__props_shorthandfmt:n #1 ,
    gloss           .tl_set:N  = \l__props_gloss_tl ,
    gloss~format    .cs_set:Np = \l__props_glossfmt:n #1 ,
    crefname        .tl_set:N  = \l__props_crefname_tl ,
    reset           .bool_set:N = \l__props_reset_bool ,
    reset           .default:n  = { true } ,
    macro           .tl_set:N  = \l__props_decl_macro_tl ,
    %% Global-only keys (list dims, spacing, etc.) are silently ignored
    %% when a style is applied at item level.
    unknown         .code:n    = {} ,
  }

% ====================================================================
% Helper: define a macro command for a style
% ====================================================================

\cs_new_protected:Nn \__props_define_macro:Nn
  {
    %% #1 = control sequence (e.g. \litem), #2 = style name
    \DeclareDocumentCommand #1 { o }
      {
        \IfValueTF { ##1 }
          {
            %% If the argument has no =, treat it as a bare name
            %% so catcodes (e.g. $math$) are preserved.
            \tl_if_in:nnTF { ##1 } { = }
              { \item [ style=#2, ##1 ] }
              { \item [ style=#2, name={##1} ] }
          }
          { \item [ style=#2 ] }
      }
  }

% ====================================================================
% Helper: store style preset (parent + overrides)
% ====================================================================

\cs_new_protected:Nn \__props_store_style:n
  {
    %% #1 = style name.
    %% Reads parent from \l__props_decl_parent_tl and
    %% overrides from \l__props_decl_overrides_tl (not passed
    %% through arguments, to preserve # tokens in format keys).
    \__props_style_ensure:n { #1 }
    \tl_set_eq:cN { g__props_style_ #1 _parent_tl }    \l__props_decl_parent_tl
    \tl_set_eq:cN { g__props_style_ #1 _overrides_tl } \l__props_decl_overrides_tl
  }

% ====================================================================
% Helper: reset local state to defaults for style resolution
% ====================================================================

% Set all per-item locals to their defaults.  Called at the start
% of item resolution, before the style chain is loaded.
\cs_new_protected:Nn \__props_decl_reset:
  {
    \tl_set:Nn  \l__props_alignment_tl { left }
    \tl_clear:N \l__props_pi_labelwidth_tl
    \tl_clear:N \l__props_pi_labelsep_tl
    \tl_clear:N \l__props_pi_itemindent_tl
    \tl_clear:N \l__props_pi_labelindent_tl
    \tl_set:Nn  \l__props_counter_tl   { none }
    \bool_set_false:N \l__props_has_counter_format_bool
    \cs_set:Npn \l__props_counterfmt:n ##1   { }
    \cs_set:Npn \l__props_displayfmt:n ##1   { ##1 }
    \cs_set:Npn \l__props_labelfmt:n ##1    { ##1 }
    \cs_set:Npn \l__props_reffmt:n ##1      { ##1 }
    \cs_set:Npn \l__props_shorthandfmt:n ##1 { ~ [##1] }
    \cs_set:Npn \l__props_glossfmt:n ##1    { ~ (##1) }
    \tl_clear:N \l__props_name_tl
    \tl_clear:N \l__props_ref_tl
    \tl_clear:N \l__props_shorthand_tl
    \tl_clear:N \l__props_gloss_tl
    \tl_clear:N \l__props_crefname_tl
    \tl_clear:N \l__props_label_tl
    \bool_set_true:N \l__props_reset_bool
  }

% ====================================================================
% Special-keys keyspace: extracts \texttt{style=} and \texttt{macro=}
% from the key-value input, leaving the rest as overrides.
% ====================================================================

\tl_new:N   \l__props_decl_parent_tl
\tl_new:N   \l__props_decl_overrides_tl

\keys_define:nn { props / declare-style-special }
  {
    style  .tl_set:N = \l__props_decl_parent_tl ,
    macro  .tl_set:N = \l__props_decl_macro_tl ,
  }

% ====================================================================
% \cs{SetPropStyle}\marg{name}\marg{key=value}
% ====================================================================

\NewDocumentCommand \SetPropStyle { m m }
  {
    %% Separate style= and macro= from the rest.
    \tl_clear:N \l__props_decl_parent_tl
    \tl_clear:N \l__props_decl_macro_tl
    \keys_set_known:nnN { props / declare-style-special }
      { #2 } \l__props_decl_overrides_tl
    %% If the style already exists and no new parent was given,
    %% preserve existing parent and prepend existing overrides
    %% so that unspecified keys keep their previous values.
    \tl_if_exist:cT { g__props_style_ #1 _parent_tl }
      {
        \tl_if_empty:NT \l__props_decl_parent_tl
          {
            \tl_set_eq:Nc \l__props_decl_parent_tl
              { g__props_style_ #1 _parent_tl }
          }
        \tl_set_eq:Nc \l_tmpa_tl { g__props_style_ #1 _overrides_tl }
        \tl_if_empty:NF \l_tmpa_tl
          {
            \tl_put_left:Nn \l__props_decl_overrides_tl { , }
            \tl_put_left:NV \l__props_decl_overrides_tl \l_tmpa_tl
          }
      }
    %% Store parent + merged overrides.
    \__props_store_style:n { #1 }
    %% Create macro command if specified.
    \tl_if_empty:NF \l__props_decl_macro_tl
      { \exp_args:NV \__props_define_macro:Nn \l__props_decl_macro_tl { #1 } }
    %% If this is the equation style and hooks are active, sync them.
    \str_if_eq:nnT { #1 } { equation }
      { \bool_if:NT \g__props_eqhooks_bool { \__props_sync_equation_hooks: } }
  }

% ====================================================================
% l3keys: special keys for \cs{DeclareNumberedStyle}
% ====================================================================

\tl_new:N \l__props_numdecl_parent_tl

\keys_define:nn { props / declare-numbered-special }
  {
    parent          .tl_set:N  = \l__props_numdecl_parent_tl ,
    macro           .tl_set:N  = \l__props_decl_macro_tl ,
  }

% ====================================================================
% \cs{DeclareNumberedStyle}\marg{name}\oarg{keys}
% ====================================================================

\NewDocumentCommand \DeclareNumberedStyle { m O{} }
  {
    %% Separate side-effect keys (parent, macro) from overrides.
    \tl_clear:N \l__props_numdecl_parent_tl
    \tl_clear:N \l__props_decl_macro_tl
    \keys_set_known:nnN { props / declare-numbered-special }
      { #2 } \l__props_decl_overrides_tl
    %% Create counter
    \newcounter { #1 }
    %% Set parent counter
    \tl_if_empty:NF \l__props_numdecl_parent_tl
      { \exp_args:NnV \@addtoreset { #1 } \l__props_numdecl_parent_tl }
    %% Define \the<counter> (default: stylename + arabic)
    \cs_gset:cpn { the#1 } { #1 \arabic{#1} }
    %% Register as a style.
    %% Prepend format=(#1) as default (user keys override it).
    %% Append counter=<name> so it always wins (the counter IS the style name).
    \tl_clear:N \l__props_decl_parent_tl
    \tl_put_left:Nn \l__props_decl_overrides_tl { format=(##1), }
    \tl_put_right:Nn \l__props_decl_overrides_tl { , counter=#1 }
    \__props_store_style:n { #1 }
    %% Define macro command if specified
    \tl_if_empty:NF \l__props_decl_macro_tl
      { \exp_args:NV \__props_define_macro:Nn \l__props_decl_macro_tl { #1 } }
  }

% ====================================================================
% l3keys: keys for \item (within prop/inlineprop)
% ====================================================================

\keys_define:nn { props / item }
  {
    name        .tl_set:N = \l__props_name_tl ,
    style       .code:n =
      {
        \tl_set:Nn \l__props_style_tl { #1 }
        \bool_if:NT \l__props_loading_defaults_bool
          {
            \tl_set:Nx \l__props_style_tl { \l__props_style_tl }
            \tl_if_empty:NF \l__props_style_tl { \__props_style_load: }
          }
      } ,
    counter     .tl_set:N = \l__props_counter_tl ,
    counter~format .code:n =
      {
        \bool_set_true:N \l__props_has_counter_format_bool
        \cs_set:Npn \l__props_counterfmt:n ##1 { #1 }
      } ,
    align       .tl_set:N = \l__props_alignment_tl ,
    labelwidth  .tl_set:N = \l__props_pi_labelwidth_tl ,
    labelsep    .tl_set:N = \l__props_pi_labelsep_tl ,
    itemindent  .tl_set:N = \l__props_pi_itemindent_tl ,
    labelindent .tl_set:N = \l__props_pi_labelindent_tl ,
    ref         .code:n =
      {
        \tl_set:Nn \l__props_ref_tl { #1 }
      } ,
    name~format     .cs_set:Np = \l__props_displayfmt:n #1 ,
    display~format  .cs_set:Np = \l__props_displayfmt:n #1 ,
    label~format    .cs_set:Np = \l__props_labelfmt:n #1 ,
    ref~format      .cs_set:Np = \l__props_reffmt:n  #1 ,
    format          .code:n =
      {
        \cs_set:Npn \l__props_displayfmt:n ##1 { #1 }
        \cs_set:Npn \l__props_reffmt:n ##1 { #1 }
      } ,
    ref~append      .code:n =
      { \cs_set:Npn \l__props_reffmt:n ##1 { \parentref{#1} } } ,
    shorthand       .code:n =
      {
        \tl_set:Nn \l__props_shorthand_tl { #1 }
      } ,
    shorthand~format .cs_set:Np = \l__props_shorthandfmt:n #1 ,
    gloss           .code:n =
      {
        \tl_set:Nn \l__props_gloss_tl { #1 }
      } ,
    gloss~format    .cs_set:Np = \l__props_glossfmt:n #1 ,
    crefname        .tl_set:N = \l__props_crefname_tl ,
    label           .tl_set:N = \l__props_label_tl ,
    reset       .bool_set:N = \l__props_reset_bool ,
    reset       .default:n  = { true } ,
    %% The pass over this keyspace also sees the cascading defaults, which may
    %% carry list-level keys (leftmargin, wrapper begin, ...); those are not
    %% errors here, and \keys_set_known:nnN collects them harmlessly.  A bare
    %% proposition name (\item[P]) never reaches this handler: it is rewritten
    %% as name={P} beforehand by \__props_normalize_item_arg:Nn.
    unknown     .code:n = {} ,
  }

%% Minimal keyspace used only for the named/nameless peek: reads name= from the
%% assembled key list without any other side effects.  The name is the whole
%% test.  A counter says how an item is numbered, not that it has a name to
%% display, and the nameless style is the one designed to look right around a
%% number --- so a counter, wherever it is set, leaves the choice alone.
\keys_define:nn { props / item-peek }
  {
    name    .tl_set:N = \l__props_name_tl ,
    unknown .code:n   = {} ,
  }

% ====================================================================
% Normalising a per-item argument
% ====================================================================

% Item keys of \cs{props/item} that may legitimately be given without a
% value.  Anything else in an item argument that carries no |=| is a bare
% proposition name.
\clist_const:Nn \c__props_valueless_item_keys_clist { reset }

% Rewrite the bare name in a per-item argument as \texttt{name=\{...\}}.
% #1 = tl var to set, #2 = raw item argument.  Doing this up front is what
% lets the key pass proper use \cs{keys_set_known:nnN}, which collects the
% list-level keys of the cascading defaults harmlessly but, by design,
% never runs an \texttt{unknown} handler that could pick a name up.
%
% With no |=| anywhere the whole argument is the name, commas and all
% (|\item[Alpha, Beta]|).  Otherwise the argument is a key list, and each
% entry of it that carries no |=| is wrapped, so a bare name also works
% alongside other keys (|\item[No Overlap, align=flush]|).
\cs_new_protected:Nn \__props_normalize_item_arg:Nn
  {
    \tl_clear:N #1
    %% A blank argument must stay blank.  \item and \item[] both arrive here
    %% with nothing to say, and wrapping that as name={} would append an empty
    %% name to the key list --- overriding, rather than inheriting, a name set
    %% for the environment or by \propoptions.
    \tl_if_blank:nF { #2 }
      {
        \tl_if_in:nnTF { #2 } { = }
          {
            \clist_map_inline:nn { #2 }
              {
                \tl_if_empty:NF #1 { \tl_put_right:Nn #1 { , } }
                \__props_normalize_entry:Nn #1 { ##1 }
              }
          }
          { \__props_normalize_entry:Nn #1 { #2 } }
      }
  }

% Append one key-list entry to #1, wrapping it as \texttt{name=\{...\}}
% unless it carries a value or is a key that may stand without one.
% The comparison is a plain token-list test, mapped over the constant:
% \cs{clist_if_in:NnTF} would put the entry in a macro parameter text,
% which silently misfires for a name containing braces (|\emph{x}|).
\cs_new_protected:Nn \__props_normalize_entry:Nn
  {
    \tl_if_in:nnTF { #2 } { = }
      { \tl_put_right:Nn #1 { #2 } }
      {
        \bool_set_false:N \l__props_valueless_key_bool
        \clist_map_inline:Nn \c__props_valueless_item_keys_clist
          {
            \tl_if_eq:nnT { #2 } { ##1 }
              {
                \bool_set_true:N \l__props_valueless_key_bool
                \clist_map_break:
              }
          }
        \bool_if:NTF \l__props_valueless_key_bool
          { \tl_put_right:Nn #1 { #2 } }
          { \tl_put_right:Nn #1 { name = { #2 } } }
      }
  }

% ====================================================================
% Shared item resolution (used by both \item within prop and \ptag)
% ====================================================================

\cs_new_protected:Nn \__props_resolve_item:n
  {
    %% --- Normalise the argument: a bare name becomes name={...} ---
    \__props_normalize_item_arg:Nn \l__props_item_arg_tl { #1 }
    %% Whether this item ends up stepping its counter.  Only the environment
    %% preview needs to know (see \__props_compute_env_preview:), and it cannot
    %% work it out in advance: which counter is used, and whether a name
    %% suppresses the step, are both settled during resolution.
    \bool_set_false:N \l__props_counter_stepped_bool

    %% --- Assemble the key list ---
    %% Cascading defaults (\propoptions) then env-local defaults (this
    %% environment's argument) then the per-item argument.  Later entries
    %% override earlier ones, giving the precedence item > env-arg >
    %% \propoptions.  Built here rather than just before the key pass because
    %% the peek below has to see all three layers.
    \tl_set_eq:NN \l__props_keylist_tl \l__props_defaults_tl
    \tl_if_empty:NF \l__props_env_defaults_tl
      {
        \tl_if_empty:NF \l__props_keylist_tl
          { \tl_put_right:Nn \l__props_keylist_tl { , } }
        \tl_put_right:NV \l__props_keylist_tl \l__props_env_defaults_tl
      }
    \tl_if_empty:NF \l__props_item_arg_tl
      {
        \tl_if_empty:NF \l__props_keylist_tl
          { \tl_put_right:Nn \l__props_keylist_tl { , } }
        \tl_put_right:NV \l__props_keylist_tl \l__props_item_arg_tl
      }

    %% --- Peek: determine named vs. nameless ---
    %% A name counts wherever it comes from --- \propoptions, the environment
    %% argument or the item's own --- so that the style an item gets and the
    %% label it carries come from the same information.
    \tl_clear:N \l__props_name_tl
    \tl_if_empty:NF \l__props_keylist_tl
      {
        \exp_args:NnV \keys_set_known:nnN
          { props / item-peek } \l__props_keylist_tl \l_tmpb_tl
      }

    %% --- Select base style (named or nameless) ---
    %% Always determined; used as the first (lowest-priority) cascade layer.
    \tl_if_empty:NTF \l__props_name_tl
      {
        \bool_lazy_and:nnTF
          { \l__props_ptag_bool }
          { ! \tl_if_empty_p:N \l__props_nameless_ptag_style_tl }
          { \tl_set_eq:NN \l__props_style_tl \l__props_nameless_ptag_style_tl }
          { \tl_set_eq:NN \l__props_style_tl \l__props_nameless_style_tl }
      }
      {
        \bool_lazy_and:nnTF
          { \l__props_ptag_bool }
          { ! \tl_if_empty_p:N \l__props_named_ptag_style_tl }
          { \tl_set_eq:NN \l__props_style_tl \l__props_named_ptag_style_tl }
          { \tl_set_eq:NN \l__props_style_tl \l__props_named_style_tl }
      }

    %% --- Reset item locals to structural defaults ---
    \__props_decl_reset:

    %% --- Load base style as first cascade layer ---
    \tl_set:Nx \l__props_style_tl { \l__props_style_tl }
    \tl_if_empty:NF \l__props_style_tl { \__props_style_load: }

    %% --- Single processing pass over the key list assembled above ---
    %% With \l__props_loading_defaults_bool set, each style= entry triggers an
    %% immediate style load, cascading on top of whatever came before.
    \tl_if_empty:NF \l__props_keylist_tl
      {
        \bool_set_true:N \l__props_loading_defaults_bool
        \exp_args:NnV \keys_set_known:nnN
          { props / item } \l__props_keylist_tl \l_tmpb_tl
        \bool_set_false:N \l__props_loading_defaults_bool
      }

    %% --- Expand counter name ---
    \tl_set:Nx \l__props_counter_tl { \l__props_counter_tl }

    %% --- Determine display text ---
    %% "none" = text item (no counter); otherwise step and display.
    \tl_if_eq:NnTF \l__props_counter_tl { none }
      {
        \tl_set_eq:NN \l__props_display_text_tl \l__props_name_tl
      }
      {
        \cs_if_exist:cTF { c@ \l__props_counter_tl }
          {
            \tl_if_empty:NTF \l__props_name_tl
              {
                %% No explicit name — step the counter and format its value.
                %% In ptag mode inside a plain equation (not align/gather), the
                %% environment already stepped the counter; skip our step.
                \bool_if:NTF \l__props_ptag_bool
                  {
                    \tl_if_eq:NnTF \l__props_counter_tl { equation }
                      {
                        \ifinalign@
                          \stepcounter { \l__props_counter_tl }
                        \else \ifingather@
                          \stepcounter { \l__props_counter_tl }
                        \fi \fi
                      }
                      { \stepcounter { \l__props_counter_tl } }
                  }
                  { \stepcounter { \l__props_counter_tl } }
                \bool_set_true:N \l__props_counter_stepped_bool
                \__props_format_label_from_counter:
              }
              { }  %% Explicit name — skip counter step entirely.
            \protected@edef \l__props_display_text_tl { \l__props_name_tl }
          }
          {
            \msg_error:nnx { props } { unknown-counter }
              { \l__props_counter_tl }
            \tl_set:Nn \l__props_display_text_tl { ??? }
          }
      }

    %% --- Determine ref text ---
    %% Priority: explicit ref > shorthand > display text
    \tl_if_empty:NTF \l__props_ref_tl
      {
        \tl_if_empty:NTF \l__props_shorthand_tl
          { \tl_set_eq:NN \l__props_ref_text_tl \l__props_display_text_tl }
          { \tl_set_eq:NN \l__props_ref_text_tl \l__props_shorthand_tl }
      }
      { \tl_set_eq:NN \l__props_ref_text_tl \l__props_ref_tl }

    %% --- Build item_output_tl (display label) ---
    \__props_build_item_output:
  }

% ====================================================================
% Helpers for label formatting (shared between resolve and preview)
% ====================================================================

% Format \cs{l__props_name_tl} from the current counter value.
% Called after counter stepping and after manual counter adjustment
% in preview computation.  Assumes all format functions are set.
\cs_new_protected:Nn \__props_format_label_from_counter:
  {
    \bool_if:NTF \l__props_has_counter_format_bool
      {
        \protected@edef \l__props_name_tl
          { \l__props_counterfmt:n { \l__props_counter_tl } }
      }
      {
        \protected@edef \l__props_name_tl
          { \use:c { the \l__props_counter_tl } }
      }
  }

% Build \cs{l__props_item_output_tl} from the already-computed
% \cs{l__props_display_text_tl}, applying display format, shorthand,
% gloss, and label format.  Shared between resolve and preview.
\cs_new_protected:Nn \__props_build_item_output:
  {
    %% An item with nothing to display contributes nothing, rather than an
    %% empty display format: \item[counter=none] with no name would otherwise
    %% come out as the format's decoration wrapped around nothing --- "()" under
    %% the default nameless style.  A shorthand or gloss is still appended
    %% below, so \item[counter=none, gloss=g] keeps its gloss.
    \tl_if_empty:NTF \l__props_display_text_tl
      { \tl_clear:N \l__props_item_output_tl }
      {
        \protected@edef \l__props_item_output_tl
          { \l__props_displayfmt:n { \l__props_display_text_tl } }
      }
    \tl_if_empty:NF \l__props_shorthand_tl
      {
        \protected@edef \l_tmpa_tl
          { \l__props_shorthandfmt:n { \l__props_shorthand_tl } }
        \tl_put_right:NV \l__props_item_output_tl \l_tmpa_tl
      }
    \tl_if_empty:NF \l__props_gloss_tl
      {
        \protected@edef \l_tmpa_tl
          { \l__props_glossfmt:n { \l__props_gloss_tl } }
        \tl_put_right:NV \l__props_item_output_tl \l_tmpa_tl
      }
    \protected@edef \l__props_item_output_tl
      { \l__props_labelfmt:n { \l__props_item_output_tl } }
  }

% ====================================================================
% Core proposition-item logic (called by the local \item in prop/inlineprop)
% ====================================================================

% \__props_item_body:n {<key string>}
% Shared body: resolve keys, optionally reset sub-counter, output item.
\cs_new_protected:Nn \__props_item_body:n
  {
    \mode_if_math:T
      { \msg_error:nn { props } { item-in-math } }
    \__props_resolve_item:n { #1 }
    %% Reset the sub-level counter one level below the current level.
    %% Skipped when reset=false, enabling intertext between sub-items or
    %% continuation numbering across parent items.
    \bool_if:NT \l__props_reset_bool
      {
        \int_compare:nNnT { \g__props_level_int } = { 1 }
          { \setcounter { numpropii } { 0 } }
        \int_compare:nNnT { \g__props_level_int } = { 2 }
          { \setcounter { numpropiii } { 0 } }
        \int_compare:nNnT { \g__props_level_int } = { 3 }
          { \setcounter { numpropiv } { 0 } }
        \int_compare:nNnT { \g__props_level_int } = { 4 }
          { \setcounter { numpropv } { 0 } }
      }
    \__props_output_item:
    %% \propformlabel is deliberately NOT updated here to the label just
    %% produced.  It exists to predict the label an environment's items will
    %% carry, so that the dimension keys can be sized to it; and a style's
    %% dimension keys are read again for every item's label area, where they
    %% would then measure the previous item's label instead of the preview.
    %% Under style=fitmargin that gave each item after the first a label box
    %% sized for its predecessor, so a label that had grown a digit overflowed
    %% and shoved its own first line sideways.  Constant for the whole
    %% environment is both what the style needs and what the name says.
    \__props_set_ref:
    \tl_if_empty:NF \l__props_label_tl
      { \exp_args:NV \label \l__props_label_tl }
    %% An align=nextline label ends with \noindent, so the item body has already
    %% begun: the space that follows \item[...] in the source would be typeset.
    %% \ignorespaces has to be the last token this command leaves behind, which
    %% is why it is issued here and not where the label was output.  For the
    %% other alignments the body has not started yet and TeX drops the space
    %% itself, in vertical mode --- and in inlineprop that space is wanted, as
    %% it separates the inline label from the text.
    \bool_if:NT \l__props_nextline_bool
      { \bool_set_false:N \l__props_nextline_bool \ignorespaces }
  }

% Save the ambient (kernel) \item at load time.  When a wrapper environment
% (mdframed, center, quote, ... — all of which call \item internally during
% their own setup) is fired inside a *nested* prop, \item is still bound to
% the proposition \item command from the enclosing list, so the wrapper's
% internal \item would spuriously create a prop item.  We restore this saved
% meaning around the wrapper-begin code (see the prop/inlineprop environments).
\cs_new_eq:NN \__props_kernel_item: \item

% The proposition \item command used inside prop and inlineprop.
% Defined with xparse so the optional-argument parser correctly handles
% nested brackets (e.g. \item[name=\oref[*]{foo}]).  Assigned to \item
% locally via \cs_set_eq:NN in each environment's begin code.
\NewDocumentCommand \__props_item_cmd: { o }
  {
    \IfValueTF { #1 }
      { \__props_item_body:n { #1 } }
      { \__props_item_body:n { } }
  }

% \item is bound to this dispatcher (not directly to \__props_item_cmd:)
% inside prop/inlineprop.  It makes the proposition \item available only
% *directly* under a prop, falling back to the ambient \item inside any
% nested list (itemize, enumerate, description, quote, ...) or other
% \item-using environment.
%
% Detection: a prop sets \makelabel to \__props_makelabel:n.  Every
% \LaTeX \list / \trivlist resets \makelabel (to \@mklab or {#1->#1}), so
% inside any nested list \makelabel no longer equals \__props_makelabel:n
% and we defer to the ambient \item; only a (nested) prop sets it back.
% Unlike \@listdepth (which \texttt{minipage} reinitialises to zero, see
% latex.ltx), \makelabel is purely group-local, so this is robust even when
% the prop sits inside a box-based wrapper such as \texttt{tcolorbox}.
% Neither branch grabs the optional argument: each target does its own
% (incompatible) optional-arg scan.
\cs_new_protected:Nn \__props_item_dispatch:
  {
    \cs_if_eq:NNTF \makelabel \__props_makelabel:n
      { \__props_item_cmd: }
      { \__props_kernel_item: }
  }

% ====================================================================
% Cross-referencing: set \@currentlabel
% ====================================================================

% Build propapply-formatted ref text into \l__props_ref_result_tl.
\tl_new:N \l__props_ref_result_tl

\cs_new_protected:Nn \__props_build_ref_text:
  {
    %% Build a \propapply{template}{content} token list for the aux file.
    %% Also save the template and content globally for \lastref and the
    %% parent stacks (pushed when entering a nested prop environment).
    \protected@xdef \g__props_last_tpl_tl
      { \l__props_reffmt:n { \propfmtarg } }
    \protected@xdef \g__props_last_cnt_tl
      { \l__props_ref_text_tl }
    \protected@edef \l__props_ref_result_tl
      {
        \propapply
          { \exp_not:V \g__props_last_tpl_tl }
          { \exp_not:V \g__props_last_cnt_tl }
      }
  }

% Set the cleveref reference type of the next \c{prop@anchor} label.
%
% A per-item type has to be expressed as the cleveref \emph{alias} of
% \c{prop@anchor}, because that is the only thing \cs{label} consults.  Neither
% of the more direct routes survives: cleveref records the type in
% \cs{cref@currentlabel} when the counter is stepped, but the kernel's first-aid
% file for cleveref (|latex2e-first-aid-for-external-files.ltx|) adds a |label|
% hook that rebuilds that value from \cs{@currentcounter} and its alias on every
% \cs{label}, discarding both a hand-edited \cs{cref@currentlabel} and the type
% given to cleveref's own \cs{refstepcounter}|[type]{counter}|.
%
% The assignment is global, and made for every item: the user's \cs{label} may
% be several groups away from the \cs{item} that set the type, and the next item
% must not inherit it.
\cs_new_protected:Npn \__props_set_cref_type:n #1
  { \cs_gset:cpn { cref@prop@anchor@alias } { #1 } }

\cs_new_protected:Nn \__props_set_ref:
  {
    \__props_build_ref_text:
    \cs_set:Npx \theprop@anchor { \exp_not:V \l__props_ref_result_tl }
    \bool_if:NT \g__props_cleveref_bool
      {
        \tl_if_empty:NTF \l__props_crefname_tl
          { \__props_set_cref_type:n { prop } }
          { \exp_args:NV \__props_set_cref_type:n \l__props_crefname_tl }
      }
    \refstepcounter { prop@anchor }
  }

% ====================================================================
% Save original \ref (for \oref / \nref circularity protection)
% ====================================================================

% Must happen at begin-document so that hyperref's redefinition of
% \ref is already in place.  \oref and \nref call this saved copy
% instead of \ref, so \let\ref\oref works without circularity.
\AtBeginDocument
  { \cs_set_eq:NN \__props_orig_ref:w \ref }

% ====================================================================
% Hyperref PDF string support
% ====================================================================

\AtBeginDocument
  {
    \@ifpackageloaded { hyperref }
      {
        %% Upgrade \propapply to suppress nested hyperlinks.
        %% We disable hyperref link commands locally (within \group_begin:
        %% / \group_end:) rather than using \NoHyper / \endNoHyper, because
        %% those operate via \global assignments and break when \propapply
        %% is nested (the inner \NoHyper overwrites the saved live-link).
        \cs_set_protected:Npn \propapply #1#2
          {
            \group_begin:
            \def \hyper@link@ [##1]##2##3##4{##4\Hy@xspace@end}
            \def \hyper@@anchor ##1##2{##2\Hy@xspace@end}
            \def \hyper@link ##1##2##3{##3\Hy@xspace@end}
            \let \hyper@anchor \@gobble
            \let \hyper@anchorstart \@gobble
            \def \hyper@anchorend {\Hy@xspace@end}
            \let \hyper@linkstart \@gobbletwo
            \def \hyper@linkend {\Hy@xspace@end}
            \def \hyper@linkurl ##1##2{##1\Hy@xspace@end}
            \def \hyper@linkfile ##1##2##3{##1\Hy@xspace@end}
            \let \Hy@backout \@gobble
            \bool_if:NTF \l__props_titlecase_bool
              {
                \protected@edef \propfmtarg { #2 }
                \tl_if_head_eq_meaning:nNTF { #1 } \propapply
                  { #1 }
                  {
                    \bool_set_false:N \l__props_titlecase_bool
                    \protected@edef \l_tmpa_tl { #1 }
                    \exp_args:NV \text_titlecase_first:n \l_tmpa_tl
                  }
              }
              {
                \protected@edef \propfmtarg { #2 }
                #1
              }
            \group_end:
          }
        %% Make \autoref work for prop@anchor labels (outputs the
        %% formatted ref text with no extra prefix).
        \def \prop@anchorautorefname { }
        \pdfstringdefDisableCommands
          {
            \def \propapply #1#2{ #2 }
            \def \propfmtarg { }
            \def \Ref #1{ \ref{#1} }
            \def \oref #1{ \ref{#1} }
            \def \Oref #1{ \ref{#1} }
            \def \nref #1{ \ref{#1} }
            \def \Nref #1{ \ref{#1} }
            \def \parentref #1{ }
            \def \Parentref #1{ }
            \def \nparentref { }
            \def \nParentref { }
            \def \lastref #1{ }
            \def \Lastref #1{ }
            \def \nlastref { }
            \def \nLastref { }
          }
      }
      { }
  }

% ====================================================================
% Cleveref integration
% ====================================================================

\bool_new:N \g__props_cleveref_bool

\cs_new_protected:Nn \__props_cleveref_setup:
  {
    \bool_gset_true:N \g__props_cleveref_bool
    %% Map the prop@anchor counter to a private cleveref type "prop".  We use
    %% "prop", not "proposition", so we do not commandeer the name a user may
    %% want for their own Proposition theorems (a common \newtheorem type).
    \crefalias { prop@anchor } { prop }
    %% Empty name: \cref just outputs the formatted ref text
    \crefname  { prop } {} {}
    \Crefname  { prop } {} {}
  }

% Cleveref derives the default reference format of a type from its name in its
% own \AtBeginDocument code, so the type must be declared before that runs.
% Begin-document hooks fire in the order they were added, which makes the
% correct moment depend on the load order:
%
%   cleveref after us   our hook was added first, so it already runs ahead of
%                       cleveref's; declare the type there, once cleveref is
%                       known to be present.
%   cleveref before us  its hook is ahead of ours and a deferred declaration
%                       would arrive too late (\cref would report "reference
%                       format for label type 'prop' undefined"), so declare
%                       the type immediately instead.
\@ifpackageloaded { cleveref }
  { \__props_cleveref_setup: }
  {
    \AtBeginDocument
      { \@ifpackageloaded { cleveref } { \__props_cleveref_setup: } { } }
  }

% ====================================================================
% Equation formatting integration
% ====================================================================

% Sync the equation hooks (\cs{tagform@} and \cs{p@equation}) with the
% current definition of the \texttt{equation} prop style.
% Called automatically when \cs{SetPropStyle}\texttt{\{equation\}\{...\}}
% is used while the hooks are active.
\cs_new_protected:Nn \__props_sync_equation_hooks:
  {
    \__props_decl_reset:
    \tl_set:Nn \l__props_style_tl { equation }
    \__props_style_load:
    \cs_set_eq:NN \__props_eqdispfmt:n \l__props_displayfmt:n
    \cs_set_eq:NN \__props_eqreffmt:n  \l__props_reffmt:n
  }

\AtBeginDocument
  {
    \bool_if:NT \g__props_equations_bool
      {
        \bool_gset_true:N \g__props_eqhooks_bool
        \__props_sync_equation_hooks:
      }
    \bool_if:NT \g__props_eqhooks_bool
      {
        %% Redefine the equation "prefix" macro so that \ref{eq:foo}
        %% produces \propapply{format}{number} instead of a bare number.
        %% This makes equation refs work with \oref and \nref.
        \cs_set:cpn { p@equation } #1
          { \propapply { \__props_eqreffmt:n { \propfmtarg } } { #1 } }
        %% Redefine \tagform@ so that displayed equation tags use
        %% the display format.  \tag* (used by \ptag) bypasses this.
        \cs_set:Npn \tagform@ #1
          { \maketag@@@
              { \__props_eqdispfmt:n
                  { \ignorespaces #1 \unskip \@@italiccorr } } }
      }
  }

% ====================================================================
% Consecutive-list hook: clear the signal when paragraph text intervenes
% ====================================================================
% The para/begin hook fires whenever TeX enters horizontal mode to start
% a paragraph.  A blank source line between two prop environments does
% NOT fire it (vertical-mode \par is a no-op), so only real intervening
% text breaks the consecutive sequence — which is exactly what we want.

\AddToHook { para/begin }
  { \bool_gset_false:N \g__props_last_was_prop_bool }

% ====================================================================
% Display math level tracking
% ====================================================================
% Inside a prop/inlineprop (level > 0), every display math environment
% increments the nesting level at its start and decrements it at its
% end.  This is achieved via \everydisplay (fires for all display math,
% including all amsmath environments) plus \aftergroup to schedule the
% decrement when the display math group closes.

% For display math, we save the parent data in dedicated
% global variables and push/pop them around the math group.
% Direct \cs{seq\_gpush} in \cs{everydisplay} is unreliable
% (amsmath group nesting can corrupt the sequence), so we
% save the data, then push/pop in a protected helper.
\tl_new:N \g__props_dispmath_save_tpl_tl
\tl_new:N \g__props_dispmath_save_cnt_tl

\cs_new_protected:Nn \__props_display_start:
  {
    \int_compare:nNnT \g__props_level_int > { 0 }
      {
        %% Save current last-item data for the push.
        \tl_gset_eq:NN \g__props_dispmath_save_tpl_tl \g__props_last_tpl_tl
        \tl_gset_eq:NN \g__props_dispmath_save_cnt_tl \g__props_last_cnt_tl
        %% Push onto parent stacks using the saved copies.
        \seq_gpush:NV \g__props_parent_tpl_seq \g__props_dispmath_save_tpl_tl
        \seq_gpush:NV \g__props_parent_cnt_seq \g__props_dispmath_save_cnt_tl
        \int_gincr:N \g__props_level_int
        \aftergroup \__props_display_end:
      }
  }

\cs_new_protected:Nn \__props_display_end:
  {
    \int_gdecr:N \g__props_level_int
    \seq_gpop:NN \g__props_parent_tpl_seq \l_tmpa_tl
    \seq_gpop:NN \g__props_parent_cnt_seq \l_tmpb_tl
  }

\AtBeginDocument
  {
    \tex_everydisplay:D \expandafter
      { \tex_the:D \tex_everydisplay:D \__props_display_start: }
  }

% ====================================================================
% \ptag — proposition tag for displayed math environments
% ====================================================================

% Wrapper to call \tag* — needed because \exp_args:NV can't expand
% into a command with * directly.
\cs_new_protected:Nn \__props_tag_star:n { \tag* { #1 } }

% Deferred ref-setting for ptags.  Amsmath typesets equations in two
% passes (measuring + output); we must only set the ref on the output
% pass (\ifmeasuring@ is false) to avoid double-stepping prop@anchor.
% \#1 = ref text, \#2 = crefname (may be empty).
\cs_new_protected:Nn \__props_ptag_finish_ref:nn
  {
    \ifmeasuring@ \else
    \cs_set:Npx \theprop@anchor { \exp_not:n { #1 } }
    \bool_if:NT \g__props_cleveref_bool
      {
        \tl_if_empty:nTF { #2 }
          { \__props_set_cref_type:n { prop } }
          { \__props_set_cref_type:n { #2 } }
      }
    \refstepcounter { prop@anchor }
    \fi
  }

\NewDocumentCommand \ptag { o }
  {
    %% Enter ptag mode so \__props_resolve_item:n can adjust counter stepping
    \bool_set_true:N \l__props_ptag_bool

    %% Process keys (same resolution as \item)
    \IfValueTF { #1 }
      { \__props_resolve_item:n { #1 } }
      { \__props_resolve_item:n { } }

    \bool_set_false:N \l__props_ptag_bool

    %% Build propapply-formatted ref text
    \__props_build_ref_text:

    %% \tag* internally calls \nonumber, which decrements the equation
    %% counter.  When the ptag itself stepped that counter, we must
    %% neutralize \incr@eqnum to prevent the decrement.  For ptags using
    %% other counters (e.g. P), the equation counter should be unaffected.
    \tl_if_eq:NnT \l__props_counter_tl { equation }
      { \cs_set_eq:NN \incr@eqnum \scan_stop: }

    %% Use \tag* for amsmath integration
    \exp_args:NV \__props_tag_star:n \l__props_item_output_tl

    %% Append our ref-setting code to \df@tag.  Amsmath collects all
    %% \tag actions into \df@tag and executes them on the output pass.
    %% We piggyback on this mechanism so our \refstepcounter runs at
    %% the right time (after measuring, not during).
    \cs_gset:Npx \df@tag
      {
        \exp_not:o { \df@tag }
        \exp_not:N \__props_ptag_finish_ref:nn
          { \exp_not:V \l__props_ref_result_tl }
          { \exp_not:V \l__props_crefname_tl }
      }

    %% Handle label key via amsmath's deferred label mechanism
    \tl_if_empty:NF \l__props_label_tl
      { \exp_args:NV \label \l__props_label_tl }
  }

% ====================================================================
% Item output
% ====================================================================

% Save the standard \item at package-load time for use inside the
% output functions.  The local \item redefinition inside prop/inlineprop
% must not affect these internal calls.
\cs_new_eq:NN \__props_list_item: \item

\cs_new_protected:Nn \__props_output_item:
  {
    \bool_if:NTF \g__props_display_mode_bool
      { \__props_output_item_display: }
      { \__props_output_item_inline: }
  }

% Display mode: use \item[...] with alignment and dimension control.
% Nextline variants handle their own labelindent, so they always
% go through the alignment path.  For other alignments, per-item
% dimension keys route through the pidim handler.
%
% Zero-width label short-circuit: when the formatted label renders nothing
% (measured by typeset width, so \displayfmt producing e.g. \textbf{} on an
% empty name still counts as empty, while a deliberately sized label does
% not), emit a label-less \item.  This keeps the first line flush at the
% text margin --- no \labelsep gap or phantom indent from the flush
% \hspace push, and no empty label line from the nextline variants --- for
% every alignment.
\cs_new_protected:Nn \__props_output_item_display:
  {
    \hbox_set:Nn \l_tmpa_box { \l__props_item_output_tl }
    \dim_compare:nNnTF { \box_wd:N \l_tmpa_box } = { \c_zero_dim }
      { \__props_list_item: [ ] }
      {
        \bool_lazy_or:nnTF
          { \str_if_eq_p:Vn \l__props_alignment_tl { nextline } }
          { \str_if_eq_p:Vn \l__props_alignment_tl { flush-nextline } }
          { \__props_output_item_align: }
          {
            %% Sequential rather than \bool_lazy_any:n, whose predicates must
            %% be expandable: \__props_dim_resolve:V is protected, since a
            %% dimension value can only be expanded safely by \protected@edef.
            \bool_set_false:N \l__props_pi_any_bool
            \__props_dim_resolve:V \l__props_pi_labelindent_tl
            \bool_if:NT \l__props_dim_set_bool
              { \bool_set_true:N \l__props_pi_any_bool }
            \__props_dim_resolve:V \l__props_pi_labelwidth_tl
            \bool_if:NT \l__props_dim_set_bool
              { \bool_set_true:N \l__props_pi_any_bool }
            \__props_dim_resolve:V \l__props_pi_labelsep_tl
            \bool_if:NT \l__props_dim_set_bool
              { \bool_set_true:N \l__props_pi_any_bool }
            \__props_dim_resolve:V \l__props_pi_itemindent_tl
            \bool_if:NT \l__props_dim_set_bool
              { \bool_set_true:N \l__props_pi_any_bool }
            \bool_if:NTF \l__props_pi_any_bool
              { \__props_output_item_pidim: }
              { \__props_output_item_align: }
          }
      }
  }

% Per-item dimension positioning.
% Temporarily overrides \cs{labelwidth}, \cs{labelsep}, and/or
% \cs{itemindent} so that the \cs{item} mechanism places the label
% exactly as it would in a list with those dimensions.  After the
% \cs{item} call the original values are restored.
%
% After applying the user's per-item overrides, the five-dimension
% constraint
% $\mathit{LI}+\mathit{LW}+\mathit{LS}=
%  \texttt{\string\leftmargin}+\texttt{\string\itemindent}$
% is enforced.  The resolver tries to derive the lowest-default-priority
% dimension that the user did \emph{not} set at this level, subject to
% $\cs{labelwidth}\ge0$ and $\cs{labelsep}\ge0$.
% Default priority (most to least protected):
% \texttt{itemindent}, \texttt{labelsep},
% \texttt{leftmargin} (frozen per-item),
% \texttt{labelwidth}, \texttt{labelindent}.
% Emit the item with its label placed as \l__props_alignment_tl asks.  Covers
% the alignments that keep the label on the item's own line: left, center and
% right place it within the label box, flush pushes it past the box to the text
% margin.  nextline and flush-nextline are not handled here --- they emit a
% blank item and set the label as a paragraph of its own, and are routed
% straight to \__props_output_item_align: before any of this.
%
% Shared by both emitting paths.  The per-item path used to emit the label
% directly, which silently ignored align: an item carrying any per-item
% dimension came out left-aligned whatever was asked for, and since a style's
% labelwidth or labelindent is a per-item key, that was every item of a
% fitmargin list.
\cs_new_protected:Nn \__props_emit_aligned_item:
  {
    \str_if_eq:VnTF \l__props_alignment_tl { flush }
      {
        %% Push label past the label area so it sits at the text margin.
        \__props_list_item: [ \hspace{\labelwidth} \hspace{\labelsep}
                \l__props_item_output_tl \hspace{\labelsep} ]
      }
      {
        %% Centred and right-aligned labels differ from the default only in
        %% how \makelabel fills the box, so set that, emit, and put it back.
        \str_if_eq:VnT \l__props_alignment_tl { center }
          { \cs_set:Nn \__props_display_label:n { \hss \mbox{##1} \hss } }
        \str_if_eq:VnT \l__props_alignment_tl { right }
          { \cs_set:Nn \__props_display_label:n { \hss \mbox{##1} } }
        \__props_list_item: [ \l__props_item_output_tl ]
        \cs_set:Nn \__props_display_label:n { \mbox{##1} \hfill }
      }
  }

\cs_new_protected:Nn \__props_output_item_pidim:
  {
    %% Save current list dimensions.
    \dim_set:Nn \l__props_save_labelwidth_dim { \labelwidth }
    \dim_set:Nn \l__props_save_labelsep_dim   { \labelsep }
    \dim_set:Nn \l__props_save_itemindent_dim { \itemindent }
    %% Baseline effective labelindent (before per-item overrides).
    \dim_set:Nn \l_tmpa_dim
      { \leftmargin + \itemindent - \labelwidth - \labelsep }
    %% Apply per-item overrides to registers.
    \__props_dim_resolve:V \l__props_pi_labelwidth_tl
    \bool_if:NT \l__props_dim_set_bool
      { \setlength { \labelwidth } { \l__props_dim_resolved_tl } }
    \__props_dim_resolve:V \l__props_pi_labelsep_tl
    \bool_if:NT \l__props_dim_set_bool
      { \setlength { \labelsep } { \l__props_dim_resolved_tl } }
    \__props_dim_resolve:V \l__props_pi_itemindent_tl
    \bool_if:NT \l__props_dim_set_bool
      { \setlength { \itemindent } { \l__props_dim_resolved_tl } }
    %% If labelindent overridden, use it; else keep baseline.
    \__props_dim_resolve:V \l__props_pi_labelindent_tl
    \bool_if:NT \l__props_dim_set_bool
      { \dim_set:Nn \l_tmpa_dim { \l__props_dim_resolved_tl } }
    %% Compute deficit = LI + LW + LS - LM - II.
    \dim_set:Nn \l_tmpb_dim
      { \l_tmpa_dim + \labelwidth + \labelsep
        - \leftmargin - \itemindent }
    %% Resolve: try non-user-set candidates in reverse default
    %% priority.  LM is frozen; LI is not a register.
    %% Default priority (most→least protected):
    %%   itemindent(1), labelsep(2), leftmargin(3, frozen),
    %%   labelwidth(4), labelindent(5, not a register).
    %% Per-item candidates: LW (pos 4), LS (pos 2), II (pos 1).
    %% For LW and LS the resolved value must be non-negative.
    %% A dimension counts as "user-set" if overridden at either
    %% the per-item level (pi_ variable) or the global level
    %% (propoptions / package option / environment option).
    \dim_compare:nNnF \l_tmpb_dim = { \c_zero_dim }
      {
        %% Try labelwidth (position 4)
        \__props_dim_resolve:V \l__props_pi_labelwidth_tl
        \bool_if:NF \l__props_dim_set_bool
          {
            \__props_dim_resolve:V \l__props_labelwidth_tl
            \bool_if:NF \l__props_dim_set_bool
              {
                \dim_compare:nNnF
                  { \labelwidth - \l_tmpb_dim } < { \c_zero_dim }
                  {
                    \dim_sub:Nn \labelwidth { \l_tmpb_dim }
                    \dim_zero:N \l_tmpb_dim
                  }
              }
          }
        %% Try labelsep (position 2) — non-negative
        \dim_compare:nNnF \l_tmpb_dim = { \c_zero_dim }
          {
            \__props_dim_resolve:V \l__props_pi_labelsep_tl
            \bool_if:NF \l__props_dim_set_bool
              {
                \__props_dim_resolve:V \l__props_labelsep_tl
                \bool_if:NF \l__props_dim_set_bool
                  {
                    \dim_compare:nNnF
                      { \labelsep - \l_tmpb_dim } < { \c_zero_dim }
                      {
                        \dim_sub:Nn \labelsep { \l_tmpb_dim }
                        \dim_zero:N \l_tmpb_dim
                      }
                  }
              }
          }
        %% Try itemindent (position 1) — no sign constraint
        \dim_compare:nNnF \l_tmpb_dim = { \c_zero_dim }
          {
            \__props_dim_resolve:V \l__props_pi_itemindent_tl
            \bool_if:NF \l__props_dim_set_bool
              {
                \__props_dim_resolve:V \l__props_itemindent_tl
                \bool_if:NF \l__props_dim_set_bool
                  {
                    \dim_add:Nn \itemindent { \l_tmpb_dim }
                    \dim_zero:N \l_tmpb_dim
                  }
              }
          }
        %% Fallback: all three candidates user-set.
        %% Use default priority ignoring user-set status.
        \dim_compare:nNnF \l_tmpb_dim = { \c_zero_dim }
          {
            \dim_compare:nNnTF
              { \labelwidth - \l_tmpb_dim } < { \c_zero_dim }
              {
                \dim_compare:nNnTF
                  { \labelsep - \l_tmpb_dim } < { \c_zero_dim }
                  { \dim_add:Nn \itemindent { \l_tmpb_dim } }
                  { \dim_sub:Nn \labelsep { \l_tmpb_dim } }
              }
              { \dim_sub:Nn \labelwidth { \l_tmpb_dim } }
          }
      }
    %% Emit list item with resolved dimensions, placed as align asks.
    \__props_emit_aligned_item:
    %% Restore original dimensions.
    \setlength { \labelwidth } { \l__props_save_labelwidth_dim }
    \setlength { \labelsep }   { \l__props_save_labelsep_dim }
    \setlength { \itemindent } { \l__props_save_itemindent_dim }
  }

% Begin the item body on the next line, unindented, after a label that has
% just taken a line of its own.
%
% Not \noindent, which starts a paragraph on the spot.  That is right when the
% body is text --- the text joins the paragraph, flush --- but wrong when the
% body opens with vertical material, a nested prop being the obvious case: the
% inner \begin{list} closes the paragraph immediately, and an empty paragraph
% is a line of white space.  So a nextline label followed by a sublist used to
% be separated from it by a blank line, while the same label followed by text
% was not.
%
% \@afterheading arms \everypar to unindent whichever paragraph comes next
% instead of starting one now, which is what \LaTeX{} itself does after a
% sectioning command for exactly this reason.  Text still starts flush; a list
% starts no paragraph, so there is none to leave empty.  It also sets
% \@nobreaktrue, which keeps a page break out from between the label and its
% body --- wanted here, the two being one item.
\cs_new_protected:Nn \__props_start_body_unindented:
  { \@afterindentfalse \@afterheading }

% Alignment-based label placement (no per-item dim overrides).
% The two alignments that give the label a line of its own are handled here;
% everything else is \__props_emit_aligned_item:, shared with the per-item
% path so that the two cannot disagree about what an alignment means.
\cs_new_protected:Nn \__props_output_item_align:
  {
    \str_if_eq:VnTF \l__props_alignment_tl { nextline }
      {
        %% Label on own line(s).  When per-item labelindent is set,
        %% the label starts at that distance from the enclosing margin.
        %% Otherwise, the label starts at the standard label position
        %% (which already reflects any global labelindent setting).
        \__props_list_item: []
        { \tl_if_empty:NTF \l__props_pi_labelindent_tl
            { \leftskip = \dimexpr \itemindent
                - \labelwidth - \labelsep \relax }
            { \leftskip = \dimexpr \l__props_pi_labelindent_tl
                - \leftmargin \relax }
          \l__props_item_output_tl \par }
        \vspace { -\parsep } \__props_start_body_unindented:
        \bool_set_true:N \l__props_nextline_bool
      }
      {
        \str_if_eq:VnTF \l__props_alignment_tl { flush-nextline }
          {
            %% Label on own line(s), starting at the text margin.
            %% Blank list item, label as ordinary paragraph text,
            %% then cancel the inter-paragraph space.
            \__props_list_item: []
            \l__props_item_output_tl \par
            \vspace { -\parsep } \__props_start_body_unindented:
            \bool_set_true:N \l__props_nextline_bool
          }
          { \__props_emit_aligned_item: }
      }
  }

% Inline mode: just output text
\cs_new_protected:Nn \__props_output_item_inline:
  { \l__props_item_output_tl }

% ====================================================================
% \propformlabel — formatted preview label, set at \begin{prop} and
% after each \item.  Expand it in list-dimension expressions, e.g.
% leftmargin=\widthof{\propformlabel}.
% ====================================================================

\NewDocumentCommand \propformlabel { } { }

% ====================================================================
% \__props_widest:n — widen a label's digits, for measurement only
% ====================================================================
% A margin sized to \widthof{\propformlabel} tracks the label exactly, so
% consecutive environments shift back and forth as the numbers change width:
% "(9)" and "(10)" differ by 5pt in the default font.  linguex avoids this by
% measuring not the label but the widest label with the same number of digits.
% It does the same to an already-formatted label, replacing all of its
% digits by whichever single digit makes the label widest and leaving formatting
% macros, spaces and letters alone.  The result is only ever measured, never
% typeset, so the substitution is invisible.
%
% Which digit that is has to be found rather than assumed.  With tabular
% figures --- Computer Modern and most text fonts --- every digit has the same
% width and it makes no difference; but with proportional (usually oldstyle)
% figures it very much does, and 8 is not generally the answer: in EB Garamond's
% oldstyle figures 8 is only the sixth widest, 0.55pt narrower than 0, so a
% margin reserved for "(88)" leaves "(00)" to overflow it and shove the first
% line of the item body sideways --- exactly the jitter this is meant to remove.
% So each of the ten digits is tried in turn and the widest result kept.  This
% costs eleven \hbox measurements, but only where the widening is used:
% once or twice per environment, and not at all in a document that never asks
% for it.  Measuring whole variants rather than bare digits also gets the label
% measured in its own font, whatever \displayformat put it in.
%
% \protected@edef, not \tl_set:Nx: a label may contain robust commands, and
% under a plain \edef \textbf expands to \protect\textbf\space, which then
% takes the rest of the list as its argument.  And a regex, not \tl_map_...:
% expl3's tl mapping skips spaces, silently narrowing any label with one.

\tl_new:N  \l__props_widen_tl      %% the label, as given
\tl_new:N  \l__props_widen_var_tl  %% one digit-variant of it
\tl_new:N  \l__props_widest_tl     %% the widest variant so far
\box_new:N \l__props_widen_box
\dim_new:N \l__props_widen_dim

% Build the variant of \l__props_widen_tl whose digits are all #1, and keep it
% if it is wider than the widest so far.
\cs_new_protected:Nn \__props_widen_try:n
  {
    \tl_set_eq:NN \l__props_widen_var_tl \l__props_widen_tl
    \regex_replace_all:nnN { \d } { #1 } \l__props_widen_var_tl
    \hbox_set:Nn \l__props_widen_box { \l__props_widen_var_tl }
    \dim_compare:nNnT
      { \box_wd:N \l__props_widen_box } > { \l__props_widen_dim }
      {
        \dim_set:Nn \l__props_widen_dim { \box_wd:N \l__props_widen_box }
        \tl_set_eq:NN \l__props_widest_tl \l__props_widen_var_tl
      }
  }

\cs_new_protected:Nn \__props_widest:n
  {
    \group_begin:
      \protected@edef \l__props_widen_tl {#1}
      \tl_set_eq:NN \l__props_widest_tl \l__props_widen_tl
      \dim_zero:N \l__props_widen_dim
      %% A label with no digits in it is its own widest variant, and measuring
      %% it eleven times to discover that would be a waste.
      \regex_match:nVTF { \d } \l__props_widen_tl
        {
          %% 8 is tried first so that it wins a tie, which is every tie in a
          %% font with tabular figures: there the substitution is a no-op on
          %% the width, and 8 is the traditional choice.
          \__props_widen_try:n { 8 }
          \int_step_inline:nnn { 0 } { 9 }
            { \__props_widen_try:n { ##1 } }
        }
        { }
      \tl_use:N \l__props_widest_tl
    \group_end:
  }

% The preview label, widened: what a style measures to get a margin that does
% not jitter.  \widthof{\propwidestlabel} in place of \widthof{\propformlabel}
% is the whole of the difference.

\NewDocumentCommand \propwidestlabel { } { \__props_widest:n { \propformlabel } }

% ====================================================================
% \__props_compute_env_preview: — compute \propformlabel at env open.
% Resolves what a bare \item would produce with the current env defaults,
% accounting for items=n (preview shows the n-th item label so that
% e.g. leftmargin=\widthof{\propformlabel} is wide enough for all items).
% Counter steps are undone; only \propformlabel is affected.
% ====================================================================

\cs_new_protected:Nn \__props_compute_env_preview:
  {
    \group_begin:
      %% Resolve a bare item with env defaults applied.
      %% This steps the relevant counter (globally); we undo it below.
      \__props_resolve_item:n { }
      %% Adjust for items > 1: advance counter by (items-1) and reformat.
      \tl_if_eq:NnF \l__props_style_tl { none }  %% skip for text-only styles
        {
          \tl_if_eq:NnF \l__props_counter_tl { none }
            {
              \int_compare:nNnF { \l__props_env_items_int } = { 1 }
                {
                  \exp_args:Nxx \addtocounter { \l__props_counter_tl }
                    { \int_eval:n { \l__props_env_items_int - 1 } }
                  \__props_format_label_from_counter:
                  \protected@edef \l__props_display_text_tl { \l__props_name_tl }
                  \__props_build_item_output:
                }
              %% Undo exactly the steps that were made: (items-1) above, plus
              %% the one \__props_resolve_item:n made unless the item is named,
              %% in which case it made none.
              \exp_args:Nxx \addtocounter { \l__props_counter_tl }
                {
                  \int_eval:n
                    {
                      - \l__props_env_items_int
                      + \bool_if:NTF \l__props_counter_stepped_bool { 0 } { 1 }
                    }
                }
            }
        }
      %% Save preview label globally so it survives group end.
      \tl_gset_eq:NN \g__props_env_preview_label_tl \l__props_item_output_tl
    \group_end:
    %% Define \propformlabel to expand to the computed label.
    \protected@edef \propformlabel { \g__props_env_preview_label_tl }
  }

% ====================================================================
% The prop environment
% ====================================================================

% --- List dimension overrides (empty = use LaTeX default) ---
% These use local assignment so \propoptions in a group is scoped.
\tl_new:N \l__props_topsep_tl
\tl_new:N \l__props_partopsep_tl
\tl_new:N \l__props_itemsep_tl
\tl_new:N \l__props_parsep_tl
\tl_new:N \l__props_leftmargin_tl
\tl_new:N \l__props_labelwidth_tl
\tl_new:N \l__props_rightmargin_tl
\tl_new:N \l__props_labelsep_tl
\tl_new:N \l__props_itemindent_tl
\tl_new:N \l__props_listparindent_tl
\tl_new:N \l__props_labelindent_tl

% --- Wrapper (environment-level) ---
% Code injected immediately before \begin{list} (wrap begin) and
% immediately after \end{list} (wrap end), wrapping the whole list in
% another environment (e.g. mdframed).  Set via the \texttt{wrapper begin}
% / \texttt{wrapper end} keys, typically inside a style.  Local assignment,
% so an env-arg or \cs{propoptions} setting is group-scoped like the dims.
%
% Nesting is handled purely by \TeX{} grouping, with no extra state: an env
% fires \l__props_wrap_begin_tl (if non-empty), then CLEARS both wrapper
% variables inside the list group.  Nested props therefore inherit nothing
% and open a box only if they set a wrapper of their own (so identical
% boxes-in-boxes are possible when asked for, and never happen by accident).
% The wrap-end code runs after \end{list}, by which point the list group has
% closed and the variables have reverted to the values this env fired with ---
% so begin and end always match, and a \cs{propoptions} issued inside the body
% (whose assignments live in the list group) cannot leak into the closing.
\tl_new:N \l__props_wrap_begin_tl
\tl_new:N \l__props_wrap_end_tl

% \makelabel for prop lists: left-aligns the label and prevents line breaks.
% \__props_output_item_align: swaps this definition for align=center and
% align=right, so \makelabel must be bound to the indirection below rather
% than to this macro itself: \list copies \makelabel's meaning once, when the
% list is created, and would otherwise freeze the left-aligned version for
% every item in it.
\cs_new:Nn \__props_display_label:n { \mbox{#1} \hfill }

% What \makelabel is actually bound to.  Its own meaning never changes, which
% is what the item dispatcher tests for; the label alignment can vary from
% item to item because the call is resolved when the label is typeset.
\cs_new:Nn \__props_makelabel:n { \__props_display_label:n {#1} }

% --- Consecutive-list (continue) state ---
% \l__props_continue_bool: true (default) = participate in consecutive joining.
% \g__props_last_was_prop_bool: signal set at \end{prop}, cleared by
%   \begin{prop} or by the para/begin hook (intervening paragraph text).
% \g__props_suppress_topsep_bool: internal flag passed from begin-code to
%   the list parameter block and then to the post-\begin{list} fixup.
% \g__props_natural_topsepadd_skip: saved \topsep+\partopsep for restoring
%   \@topsepadd after \begin{list} so that after-spacing is unaffected.
% \g__props_prev_itemsep_parsep_skip: \itemsep+\parsep saved at \end{prop}
%   for use as the TARGET spacing by the immediately following \begin{prop}.
\bool_new:N \l__props_continue_bool
\bool_set_true:N \l__props_continue_bool
\bool_new:N \g__props_last_was_prop_bool
\bool_new:N \g__props_suppress_topsep_bool
\skip_new:N \g__props_natural_topsepadd_skip
\skip_new:N \g__props_prev_itemsep_parsep_skip

% Resolve a dimension key's value.  \#1 = the value.  Sets
% \cs{l__props_dim_resolved_tl} to the length to use and
% \cs{l__props_dim_set_bool} to whether there is one: false when the key is
% unset, and false for the sentinel |*|, which means \enquote{as if unset} ---
% inherit the class default, or leave the dimension free for the label-area
% resolver to derive from the other four.
%
% The value is expanded first, so that a level-varying value written with
% \cs{proplevelchoice} is resolved at the level being set up, and so that a
% sentinel reached through one is seen.  \cs{protected@edef}, not
% \cs{tl_set:Nx}: a value may contain robust commands, which a plain \cs{edef}
% expands to \cs{protect}\cs{cs}\verb*| | and mangles.  Expanding first is safe
% for every form a dimension takes --- lengths, register arithmetic, rubber
% lengths, \textsf{calc} expressions --- all of which \cs{setlength} computes
% identically before and after.
%
% Protected, so the tests below cannot use \cs{bool_lazy_any:n} and friends,
% which need expandable predicates.  An expandable version is not available:
% \cs{protect}-based robust commands cannot be handled without
% \cs{protected@edef}.
%
% \cs{l__props_dim_resolved_tl} is shared, so a caller that keeps a resolved
% value across a further resolve must copy it first.
\tl_new:N   \l__props_dim_resolved_tl
\bool_new:N \l__props_dim_set_bool
\cs_new_protected:Nn \__props_dim_resolve:n
  {
    \tl_clear:N \l__props_dim_resolved_tl
    \bool_set_false:N \l__props_dim_set_bool
    \tl_if_blank:nF { #1 }
      {
        \protected@edef \l__props_dim_resolved_tl { #1 }
        \str_if_eq:VnF \l__props_dim_resolved_tl { * }
          { \bool_set_true:N \l__props_dim_set_bool }
      }
  }
\cs_generate_variant:Nn \__props_dim_resolve:n { V }

% Helper: apply a dimension override.  \#1 = tl variable, \#2 = dimension.
% Nothing is assigned when the value is unset or the sentinel.
\cs_new_protected:Nn \__props_apply_dim:Nn
  {
    \__props_dim_resolve:V #1
    \bool_if:NT \l__props_dim_set_bool
      { \setlength { #2 } { \l__props_dim_resolved_tl } }
  }

% ====================================================================
% Env-local list configuration: save/restore
% ====================================================================
% The list-dimension and wrapper variables below hold the configuration a
% prop applies to its own list.  A prop argument may override them, but the
% override must not reach nested environments (an argument configures just
% this environment).  So each prop snapshots these into \l__props_ambient_*
% before reading its argument, and restores them inside the list group after
% \begin{list} --- the list itself has already used the argument values,
% while nested props see the restored (cascading / \propoptions) values.
% The ambient snapshot also feeds the operative-dimension interface.
\clist_const:Nn \c__props_env_dims_clist
  {
    leftmargin , rightmargin , topsep , partopsep , itemsep , parsep ,
    labelsep , itemindent , listparindent , labelwidth , labelindent ,
    wrap_begin , wrap_end
  }
\cs_generate_variant:Nn \tl_set_eq:NN { cc }
\clist_map_inline:Nn \c__props_env_dims_clist
  { \tl_new:c { l__props_ambient_ #1 _tl } }
\cs_new_protected:Nn \__props_env_snapshot:
  {
    \clist_map_inline:Nn \c__props_env_dims_clist
      { \tl_set_eq:cc { l__props_ambient_ ##1 _tl } { l__props_ ##1 _tl } }
    \__props_set_operative_leftmargin:
  }
\cs_new_protected:Nn \__props_env_restore:
  {
    \clist_map_inline:Nn \c__props_env_dims_clist
      { \tl_set_eq:cc { l__props_ ##1 _tl } { l__props_ambient_ ##1 _tl } }
  }

% Operative-dimension interface.  \propoperativeleftmargin is a read-only
% length holding the leftmargin an ordinary (unframed) prop would use at the
% current nesting level: the ambient \propoptions/class value, resolved exactly
% as \__props_apply_dim: resolves it, with the class default \leftmargin<level>
% standing in wherever that leaves the dimension unset.  It is recomputed from
% the ambient snapshot at every \begin{prop}, so it is valid inside a prop's
% wrapper code (before that environment's own leftmargin override has taken
% effect).
\newlength \propoperativeleftmargin
\cs_new_protected:Nn \__props_set_operative_leftmargin:
  {
    \setlength \propoperativeleftmargin
      { \proplevelchoice { \leftmargini , \leftmarginii , \leftmarginiii ,
          \leftmarginiv , \leftmarginv , \leftmarginvi } }
    \__props_dim_resolve:V \l__props_ambient_leftmargin_tl
    \bool_if:NT \l__props_dim_set_bool
      { \setlength \propoperativeleftmargin { \l__props_dim_resolved_tl } }
  }

\NewDocumentEnvironment { prop } { O{} }
  {
    \stepcounter { prop }
    \int_gincr:N \g__props_level_int
    %% Push last item's template/content onto parent stacks
    \seq_gpush:NV \g__props_parent_tpl_seq \g__props_last_tpl_tl
    \seq_gpush:NV \g__props_parent_cnt_seq \g__props_last_cnt_tl
    \bool_gset_true:N \g__props_display_mode_bool
    %% Reset per-env items= counter (not part of defaults tl).
    \int_set:Nn  \l__props_env_items_int { 1 }
    %% Snapshot the cascading list configuration, and start this environment with
    %% an empty env-local item-default layer (so the argument, read next, styles
    %% only this environment).
    \__props_env_snapshot:
    \tl_clear:N \l__props_env_defaults_tl
    %% Apply the argument.  Known global keys (dims, tightspacing, wrapper) go to
    %% the live list-config variables; unknown item-level keys and style= are
    %% routed to the env-local layer by \l__props_env_arg_bool.  Global-only keys
    %% (equations) are filtered out with a warning.
    \bool_set_true:N \l__props_env_arg_bool
    \keys_set_filter:nnnN { props / global } { global-only }
      { #1 } \l_tmpa_tl
    \bool_set_false:N \l__props_env_arg_bool
    \tl_if_empty:NF \l_tmpa_tl
      {
        \msg_warning:nnx { props } { global-only-keys }
          { \l_tmpa_tl }
      }
    %% Compute the preview label for \propformlabel (used in list dims).
    \__props_compute_env_preview:
    %% Consecutive-list joining: if the previous environment was a prop
    %% with continue=true, and this one also has continue=true, and no
    %% paragraph text has intervened (flag still set), cancel the
    %% inter-list \topsep glue and replace it with the TARGET spacing
    %% (\itemsep+\parsep saved from the previous prop).  We use
    %% \vskip -G \vskip TARGET instead of \unskip, since \unskip is
    %% not valid in outer vertical mode.  \lastskip>0 guards against
    %% page breaks: if the page builder consumed the glue we fall
    %% through gracefully with normal spacing.
    \bool_if:NT \l__props_continue_bool
      {
        \bool_if:NT \g__props_last_was_prop_bool
          {
            \dim_compare:nNnT { \lastskip } > { 0pt }
              {
                %% Temporarily borrow \g__props_natural_topsepadd_skip
                %% to store the full rubber glue for cancellation;
                %% it is properly overwritten in the parameter block.
                \skip_gset:Nn \g__props_natural_topsepadd_skip { \lastskip }
                \vskip -\g__props_natural_topsepadd_skip
                \vskip \g__props_prev_itemsep_parsep_skip
                \bool_gset_true:N \g__props_suppress_topsep_bool
              }
          }
      }
    \bool_gset_false:N \g__props_last_was_prop_bool
    %% Wrapper: open the surrounding environment (e.g. mdframed) around the
    %% whole list.  Fired here so the box encloses \begin{list}...\end{list}.
    %% Wrapper environments that call \item internally (center, quote, mdframed)
    %% are handled by the item dispatcher: their \list/\trivlist resets \makelabel,
    %% so their internal \item resolves to the ambient \item, not a prop item.
    \tl_if_empty:NF \l__props_wrap_begin_tl { \l__props_wrap_begin_tl }
    \begin{list} {}
      {
        %% \makelabel set by \cs_set_eq: (not a wrapper) so the item dispatcher
        %% can recognise a prop list by \makelabel's identity.
        \cs_set_eq:NN \makelabel \__props_makelabel:n
        %% Establish the standard \labelwidth for this list depth.  \list sets
        %% \itemindent, \rightmargin and \listparindent itself, and \@listii and
        %% deeper set \labelwidth, but at depth one \@listi does not: such a list
        %% inherits whatever \labelwidth the enclosing context happened to leave
        %% behind.  (A prop inside a wrapper box is at depth one, since the box
        %% resets the list depth; inside a description, which sets \labelwidth to
        %% zero for its own labels, it would inherit 0pt and lose its label area
        %% --- and with it the \labelsep gap after a flush label.)  itemize,
        %% enumerate and description each set \labelwidth for themselves; this is
        %% prop doing the same, using the same value \@listii would.
        %%
        %% Done unconditionally, not just when no labelwidth override follows.
        %% An override normally overwrites this outright, so the work is wasted
        %% --- except when the override resolves to the sentinel at this level,
        %% or reads \labelwidth itself, in which case nothing is assigned and
        %% this is the only value there is.
        \dim_set:Nn \labelwidth { \leftmargin - \labelsep }
        \dim_compare:nNnT \labelwidth < \c_zero_dim
          { \dim_zero:N \labelwidth }
        %% Apply dimension overrides.  Empty or the sentinel * = inherit the
        %% document class default.
        \__props_apply_dim:Nn \l__props_topsep_tl        \topsep
        \__props_apply_dim:Nn \l__props_partopsep_tl      \partopsep
        \__props_apply_dim:Nn \l__props_itemsep_tl        \itemsep
        \__props_apply_dim:Nn \l__props_parsep_tl         \parsep
        %% \labelsep before \leftmargin, since a leftmargin may be written in
        %% terms of it --- fitmargin's \widthof{\propwidestlabel}+\labelsep is
        %% the built-in case --- and would otherwise be computed from the value
        %% this list is about to replace.  With labelsep left alone the order
        %% makes no difference, which is why it went unnoticed.
        \__props_apply_dim:Nn \l__props_labelsep_tl       \labelsep
        \__props_apply_dim:Nn \l__props_leftmargin_tl     \leftmargin
        \__props_apply_dim:Nn \l__props_rightmargin_tl    \rightmargin
        \__props_apply_dim:Nn \l__props_itemindent_tl     \itemindent
        \__props_apply_dim:Nn \l__props_listparindent_tl  \listparindent
        \__props_apply_dim:Nn \l__props_labelwidth_tl     \labelwidth
        %% Constraint resolution: LI + LW + LS = LM + II.
        %% When the user sets labelindent, one of the four real
        %% registers must absorb the deficit.  The resolver tries
        %% the lowest-default-priority non-user-set dimension first,
        %% subject to LW >= 0 and LS >= 0.
        %% Default priority (most→least protected):
        %%   itemindent(1), labelsep(2), leftmargin(3),
        %%   labelwidth(4), labelindent(5).
        \__props_dim_resolve:V \l__props_labelindent_tl
        \bool_if:NT \l__props_dim_set_bool
          {
            %% Copied out of the shared \l__props_dim_resolved_tl at once: the
            %% resolves below, deciding which register may absorb the deficit,
            %% overwrite it while this value is still needed.
            \tl_set_eq:NN \l_tmpa_tl \l__props_dim_resolved_tl
            %% Compute deficit = LI + LW + LS - LM - II.
            \dim_set:Nn \l_tmpb_dim
              { \l_tmpa_tl + \labelwidth + \labelsep
                - \leftmargin - \itemindent }
            \dim_compare:nNnF \l_tmpb_dim = { \c_zero_dim }
              {
                %% Try labelwidth (position 4) — non-negative
                \__props_dim_resolve:V \l__props_labelwidth_tl
                \bool_if:NF \l__props_dim_set_bool
                  {
                    \dim_compare:nNnF
                      { \labelwidth - \l_tmpb_dim } < { \c_zero_dim }
                      {
                        \dim_sub:Nn \labelwidth { \l_tmpb_dim }
                        \dim_zero:N \l_tmpb_dim
                      }
                  }
                %% Try leftmargin (position 3) — no sign constraint
                \dim_compare:nNnF \l_tmpb_dim = { \c_zero_dim }
                  {
                    \__props_dim_resolve:V \l__props_leftmargin_tl
                    \bool_if:NF \l__props_dim_set_bool
                      {
                        \dim_add:Nn \leftmargin { \l_tmpb_dim }
                        \dim_zero:N \l_tmpb_dim
                      }
                  }
                %% Try labelsep (position 2) — non-negative
                \dim_compare:nNnF \l_tmpb_dim = { \c_zero_dim }
                  {
                    \__props_dim_resolve:V \l__props_labelsep_tl
                    \bool_if:NF \l__props_dim_set_bool
                      {
                        \dim_compare:nNnF
                          { \labelsep - \l_tmpb_dim } < { \c_zero_dim }
                          {
                            \dim_sub:Nn \labelsep { \l_tmpb_dim }
                            \dim_zero:N \l_tmpb_dim
                          }
                      }
                  }
                %% Try itemindent (position 1) — no sign constraint
                \dim_compare:nNnF \l_tmpb_dim = { \c_zero_dim }
                  {
                    \__props_dim_resolve:V \l__props_itemindent_tl
                    \bool_if:NF \l__props_dim_set_bool
                      {
                        \dim_add:Nn \itemindent { \l_tmpb_dim }
                        \dim_zero:N \l_tmpb_dim
                      }
                  }
                %% Fallback: all candidates user-set.
                %% Use default priority ignoring user-set status.
                \dim_compare:nNnF \l_tmpb_dim = { \c_zero_dim }
                  {
                    \dim_compare:nNnTF
                      { \labelwidth - \l_tmpb_dim } < { \c_zero_dim }
                      { \dim_add:Nn \leftmargin { \l_tmpb_dim } }
                      { \dim_sub:Nn \labelwidth { \l_tmpb_dim } }
                  }
              }
          }
        %% Consecutive-list: if signalled, save the natural \@topsepadd
        %% (\topsep+\partopsep, since we are entering from vmode) for
        %% after-spacing restoration, then set \topsep to TARGET so
        %% that \@trivlist's \addvspace{TARGET} sees \lastskip=TARGET
        %% (deposited by the pre-\begin{list} \vskip) and does nothing.
        %% Net before-spacing = TARGET = \g__props_prev_itemsep_parsep_skip.
        \bool_if:NT \g__props_suppress_topsep_bool
          {
            \skip_gset:Nn \g__props_natural_topsepadd_skip { \topsep }
            \skip_gadd:Nn \g__props_natural_topsepadd_skip { \partopsep }
            \setlength { \topsep } { \g__props_prev_itemsep_parsep_skip }
            \setlength { \partopsep } { \z@ }
          }
      }
    %% Restore \@topsepadd to the natural value so that \endtrivlist
    %% uses the correct (unmodified) topsep for after-spacing.
    \bool_if:NT \g__props_suppress_topsep_bool
      {
        \@topsepadd = \g__props_natural_topsepadd_skip
        \bool_gset_false:N \g__props_suppress_topsep_bool
      }
    %% Bind \item to the dispatcher, so the proposition \item applies only
    %% directly under this prop and reverts to the ambient \item inside any
    %% nested list (the dispatcher keys off \makelabel; see its definition).
    %% Local to the list group; undone automatically by \end{list}.
    \cs_set_eq:NN \item \__props_item_dispatch:
    %% Restore the cascading list configuration inside the list group.  \begin{list}
    %% above has already consumed this environment's argument values, so nested
    %% props now see the cascading (\propoptions) values, not this environment's
    %% overrides --- e.g. an argument leftmargin/wrapper does not reach sublists.
    %% \end{list} reverts the restore, so the end code still sees this env's own
    %% wrapper for the matching wrap-end.
    \__props_env_restore:
  }
  {
    %% Save this list's \itemsep+\parsep as the TARGET spacing for the
    %% immediately following \begin{prop}.  Must be done BEFORE
    %% \end{list}, because \end{list} closes the list group and
    %% restores \itemsep/\parsep to their enclosing-scope values.
    \bool_if:NT \l__props_continue_bool
      {
        \skip_gset:Nn \g__props_prev_itemsep_parsep_skip { \itemsep }
        \skip_gadd:Nn \g__props_prev_itemsep_parsep_skip { \parsep }
      }
    \end{list}
    %% Wrapper: close the surrounding environment.  \end{list} has just restored
    %% \l__props_wrap_end_tl to the value this env fired \l__props_wrap_begin_tl
    %% with (the in-list clear reverted), so this matches the opening.
    \tl_if_empty:NF \l__props_wrap_end_tl { \l__props_wrap_end_tl }
    %% Pop parent stacks.  At level >= 2, restore the popped values
    %% into \g__props_last_* so that re-entering a prop for intertext
    %% sees the correct parent (not a stale sub-item).
    \seq_gpop:NN \g__props_parent_tpl_seq \l_tmpa_tl
    \seq_gpop:NN \g__props_parent_cnt_seq \l_tmpb_tl
    %% At level >= 2, restore the popped parent values into
    %% \g__props_last_* so that re-entering a prop for intertext
    %% sees the correct parent (not a stale sub-item).
    \int_compare:nNnT { \g__props_level_int } > { 1 }
      {
        \tl_gset_eq:NN \g__props_last_tpl_tl \l_tmpa_tl
        \tl_gset_eq:NN \g__props_last_cnt_tl \l_tmpb_tl
      }
    \int_gdecr:N \g__props_level_int
    %% Restore display_mode: true if we're still inside an outer prop,
    %% false if we've exited to top level (or into an inlineprop).
    \int_compare:nNnTF { \g__props_level_int } > { 0 }
      { \bool_gset_true:N \g__props_display_mode_bool }
      { \bool_gset_false:N \g__props_display_mode_bool }
    %% Signal that the next prop may join seamlessly (cleared by
    %% \begin{prop} or by the para/begin hook if text intervenes).
    %% continue=false suppresses it, which is how the framed style keeps a
    %% frame clear of whatever follows it.
    \bool_if:NT \l__props_continue_bool
      { \bool_gset_true:N \g__props_last_was_prop_bool }
  }

% ====================================================================
% The inlineprop environment
% ====================================================================

\NewDocumentEnvironment { inlineprop } { O{} }
  {
    \stepcounter { prop }
    \int_gincr:N \g__props_level_int
    %% Push last item's template/content onto parent stacks
    \seq_gpush:NV \g__props_parent_tpl_seq \g__props_last_tpl_tl
    \seq_gpush:NV \g__props_parent_cnt_seq \g__props_last_cnt_tl
    %% Reset per-env items= counter (not part of defaults tl).
    \int_set:Nn  \l__props_env_items_int { 1 }
    %% Snapshot cascading config and reset the env-local item layer (same as prop).
    \__props_env_snapshot:
    \tl_clear:N \l__props_env_defaults_tl
    %% Apply the argument (env-local routing on).
    \bool_set_true:N \l__props_env_arg_bool
    \keys_set_filter:nnnN { props / global } { global-only }
      { #1 } \l_tmpa_tl
    \bool_set_false:N \l__props_env_arg_bool
    \tl_if_empty:NF \l_tmpa_tl
      {
        \msg_warning:nnx { props } { global-only-keys }
          { \l_tmpa_tl }
      }
    %% Compute the preview label for \propformlabel.
    \__props_compute_env_preview:
    %% Wrapper: open the surrounding environment around the inline content.
    \tl_if_empty:NF \l__props_wrap_begin_tl { \l__props_wrap_begin_tl }
    %% inlineprop opens no list, so provide an explicit group to play the list
    %% group's role: restoring the cascading config inside it stops nested props
    %% inheriting this environment's overrides, and \group_end: in the end-code
    %% reverts the restore so the matching wrap-end sees this env's own wrapper.
    \group_begin:
    \__props_env_restore:
    %% Bind \item to the dispatcher.  inlineprop opens no list, so set \makelabel
    %% to the prop label maker by hand (it is what the dispatcher keys off); a
    %% nested list resets \makelabel and the dispatcher reverts to ambient \item.
    \cs_set_eq:NN \makelabel \__props_makelabel:n
    \cs_set_eq:NN \item \__props_item_dispatch:
  }
  {
    %% Close the wrapper group (restoring the wrapper variables), then run the
    %% matching wrap-end code.
    \group_end:
    \tl_if_empty:NF \l__props_wrap_end_tl { \l__props_wrap_end_tl }
    %% Pop parent stacks (same restore logic as prop environment)
    \seq_gpop:NN \g__props_parent_tpl_seq \l_tmpa_tl
    \seq_gpop:NN \g__props_parent_cnt_seq \l_tmpb_tl
    \int_compare:nNnT { \g__props_level_int } > { 1 }
      {
        \tl_gset_eq:NN \g__props_last_tpl_tl \l_tmpa_tl
        \tl_gset_eq:NN \g__props_last_cnt_tl \l_tmpb_tl
      }
    \int_gdecr:N \g__props_level_int
  }

% ====================================================================
% \oref — ref with optional prefix/suffix
% ====================================================================

% Helper: locally redefine \propapply to inject prefix (#1) and
% suffix (#2) into the content slot.  Uses \cs_set_protected:Npx to
% freeze the prefix/suffix values at definition time.
\cs_new_protected:Nn \__props_oref_setup:nn
  {
    \tl_set:Nn \l_tmpa_tl { #1 }
    \tl_set:Nn \l_tmpb_tl { #2 }
    %% Save the current (standard) \propapply so we can restore it
    %% inside the redefined version.  This ensures prefix/suffix only
    %% apply at the outermost \propapply; any nested \propapply from
    %% \parentref etc. uses the standard definition.
    %% Delegation to the saved version also ensures that hyperlink
    %% suppression and titlecase handling are applied correctly.
    \cs_set_eq:NN \__props_std_propapply:ww \propapply
    \cs_set_protected:Npx \propapply ##1##2
      {
        \exp_not:N \cs_set_eq:NN \exp_not:N \propapply
          \exp_not:N \__props_std_propapply:ww
        \exp_not:N \__props_std_propapply:ww
          { ##1 }
          { \exp_not:V \l_tmpa_tl ##2 \exp_not:V \l_tmpb_tl }
      }
  }

\NewDocumentCommand \oref { s o o m }
  {
    \group_begin:
    \IfValueTF { #3 }
      { \__props_oref_setup:nn { #2 } { #3 } }
      {
        \IfValueT { #2 }
          { \__props_oref_setup:nn { } { #2 } }
      }
    \IfBooleanTF { #1 }
      { \__props_orig_ref:w * { #4 } }
      { \__props_orig_ref:w   { #4 } }
    \group_end:
  }

% ====================================================================
% \nref — naked ref (strips formatting)
% ====================================================================

\NewDocumentCommand \nref { s m }
  {
    \group_begin:
    \cs_set:Npn \propapply ##1##2 { ##2 }
    \IfBooleanTF { #1 }
      { \__props_orig_ref:w * { #2 } }
      { \__props_orig_ref:w   { #2 } }
    \group_end:
  }

% ====================================================================
% \Ref — titlecase ref
% ====================================================================

% Overrides the LaTeX kernel's \Ref, which does not understand
% \propapply.  For non-propositions labels (equations, sections, etc.)
% \Ref behaves like \ref (no titlecasing); use \MakeUppercase{\ref{..}}
% for those if needed.  Deferred to \AtBeginDocument because the kernel
% re-establishes its own \Ref during \begin{document}; our definition
% must come after that.
\AtBeginDocument
  {
    \DeclareDocumentCommand \Ref { s m }
      {
        \group_begin:
        \bool_set_true:N \l__props_titlecase_bool
        \IfBooleanTF { #1 }
          { \__props_orig_ref:w * { #2 } }
          { \__props_orig_ref:w   { #2 } }
        \group_end:
      }
  }

% ====================================================================
% \Oref — titlecase ref with optional prefix/suffix
% ====================================================================

\NewDocumentCommand \Oref { s o o m }
  {
    \group_begin:
    \bool_set_true:N \l__props_titlecase_bool
    \IfValueTF { #3 }
      { \__props_oref_setup:nn { #2 } { #3 } }
      {
        \IfValueT { #2 }
          { \__props_oref_setup:nn { } { #2 } }
      }
    \IfBooleanTF { #1 }
      { \__props_orig_ref:w * { #4 } }
      { \__props_orig_ref:w   { #4 } }
    \group_end:
  }

% ====================================================================
% \Nref — titlecase naked ref
% ====================================================================

\NewDocumentCommand \Nref { s m }
  {
    \group_begin:
    \cs_set:Npn \propapply ##1##2 { \text_titlecase_first:n { ##2 } }
    \IfBooleanTF { #1 }
      { \__props_orig_ref:w * { #2 } }
      { \__props_orig_ref:w   { #2 } }
    \group_end:
  }

% ====================================================================
% props/dims-only — keyspace for dim-only style application.
% Has the same list-dimension and spacing handlers as props/global, but
% its unknown handler is a no-op, so item-level keys in a style's
% overrides are silently ignored.  Used by \__props_style_apply_dims:n.
% (Defined here, after all dim tl variables are declared.)
% ====================================================================

\keys_define:nn { props / dims-only }
  {
    style             .code:n      = { \__props_style_apply_dims:n { #1 } } ,
    tightspacing      .code:n      =
      {
        \tl_set:Nn \l__props_topsep_tl     { 2\p@ \@plus\p@ \@minus\p@ }
        \tl_set:Nn \l__props_itemsep_tl    { 2\p@ \@plus\p@ \@minus\p@ }
        \tl_set:Nn \l__props_parsep_tl     { \z@ }
        \tl_set:Nn \l__props_partopsep_tl  { \p@ \@plus\z@ \@minus\p@ }
      } ,
    nosep             .code:n      =
      {
        \tl_set:Nn \l__props_topsep_tl  { 0pt }
        \tl_set:Nn \l__props_itemsep_tl { 0pt }
        \tl_set:Nn \l__props_parsep_tl  { 0pt }
      } ,
    continue          .bool_set:N  = \l__props_continue_bool ,
    continue          .default:n   = { true } ,
    items             .int_set:N   = \l__props_env_items_int ,
    topsep            .tl_set:N    = \l__props_topsep_tl ,
    partopsep         .tl_set:N    = \l__props_partopsep_tl ,
    itemsep           .tl_set:N    = \l__props_itemsep_tl ,
    parsep            .tl_set:N    = \l__props_parsep_tl ,
    leftmargin        .tl_set:N    = \l__props_leftmargin_tl ,
    rightmargin       .tl_set:N    = \l__props_rightmargin_tl ,
    labelwidth        .tl_set:N    = \l__props_labelwidth_tl ,
    labelsep          .tl_set:N    = \l__props_labelsep_tl ,
    itemindent        .tl_set:N    = \l__props_itemindent_tl ,
    listparindent     .tl_set:N    = \l__props_listparindent_tl ,
    labelindent       .tl_set:N    = \l__props_labelindent_tl ,
    wrapper~begin     .tl_set:N    = \l__props_wrap_begin_tl ,
    wrapper~end       .tl_set:N    = \l__props_wrap_end_tl ,
    unknown           .code:n      = {} ,
  }

% ====================================================================
% \__props_style_apply_dims:n — walk a style's parent chain and apply
% only its list-dimension overrides (topsep, itemsep, leftmargin, etc.)
% through props/dims-only.  Item-level keys are silently ignored.
% Called by the style= handler in props/global so that dimension effects
% take effect at \begin{prop} time; style= itself is stored lazily in
% \l__props_defaults_tl for evaluation at item-resolve time.
% ====================================================================

\cs_new_protected:Nn \__props_style_apply_dims:n
  {
    \tl_if_exist:cT { g__props_style_ #1 _parent_tl }
      {
        %% Apply parent chain first.
        \tl_set_eq:Nc \l_tmpa_tl { g__props_style_ #1 _parent_tl }
        \tl_if_empty:NF \l_tmpa_tl
          {
            \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl }
            \exp_args:NV \__props_style_apply_dims:n \l_tmpa_tl
          }
        %% Then apply this style's overrides through props/dims-only.
        \tl_set_eq:Nc \l_tmpa_tl { g__props_style_ #1 _overrides_tl }
        \tl_if_empty:NF \l_tmpa_tl
          { \exp_args:NnV \keys_set:nn { props / dims-only } \l_tmpa_tl }
      }
  }

% Append an item-level key entry to the active item-default layer: the
% env-local layer while a prop argument is being read, the cascading layer
% (\propoptions) otherwise.
\cs_new_protected:Nn \__props_defaults_append:n
  {
    \bool_if:NTF \l__props_env_arg_bool
      {
        \tl_if_empty:NF \l__props_env_defaults_tl
          { \tl_put_right:Nn \l__props_env_defaults_tl { , } }
        \tl_put_right:Nn \l__props_env_defaults_tl { #1 }
      }
      {
        \tl_if_empty:NF \l__props_defaults_tl
          { \tl_put_right:Nn \l__props_defaults_tl { , } }
        \tl_put_right:Nn \l__props_defaults_tl { #1 }
      }
  }

% ====================================================================
% \propoptions — global configuration
% ====================================================================

\keys_define:nn { props / global }
  {
    named~style               .tl_set:N = \l__props_named_style_tl ,
    named~ptag~style          .tl_set:N = \l__props_named_ptag_style_tl ,
    nameless~style            .tl_set:N = \l__props_nameless_style_tl ,
    nameless~ptag~style       .tl_set:N = \l__props_nameless_ptag_style_tl ,
    equations         .code:n      =
      {
        \bool_gset_true:N \g__props_equations_bool
        \bool_gset_true:N \g__props_eqhooks_bool
        \tl_set:Nn \l__props_nameless_style_tl { eqnum }
      } ,
    equations         .default:n   = { true } ,
    equations         .groups:n    = { global-only } ,
    style             .code:n      =
      {
        %% Apply dim keys from the style chain eagerly (they affect \begin{prop}).
        %% Store style=X lazily in the active item-default layer for item-time
        %% evaluation (\proplevelchoice resolves at the correct nesting depth).
        \__props_style_apply_dims:n { #1 }
        \__props_defaults_append:n { style = { #1 } }
      } ,
    items             .int_set:N   = \l__props_env_items_int ,
    tightspacing      .code:n      =
      {
        \tl_set:Nn \l__props_topsep_tl     { 2\p@ \@plus\p@ \@minus\p@ }
        \tl_set:Nn \l__props_itemsep_tl    { 2\p@ \@plus\p@ \@minus\p@ }
        \tl_set:Nn \l__props_parsep_tl     { \z@ }
        \tl_set:Nn \l__props_partopsep_tl  { \p@ \@plus\z@ \@minus\p@ }
      } ,
    nosep             .code:n      =
      {
        \tl_set:Nn \l__props_topsep_tl  { 0pt }
        \tl_set:Nn \l__props_itemsep_tl { 0pt }
        \tl_set:Nn \l__props_parsep_tl  { 0pt }
      } ,
    continue          .bool_set:N  = \l__props_continue_bool ,
    continue          .default:n   = { true } ,
    %% List dimensions
    topsep            .tl_set:N    = \l__props_topsep_tl ,
    partopsep         .tl_set:N    = \l__props_partopsep_tl ,
    itemsep           .tl_set:N    = \l__props_itemsep_tl ,
    parsep            .tl_set:N    = \l__props_parsep_tl ,
    leftmargin        .tl_set:N    = \l__props_leftmargin_tl ,
    rightmargin       .tl_set:N    = \l__props_rightmargin_tl ,
    labelwidth        .tl_set:N    = \l__props_labelwidth_tl ,
    labelsep          .tl_set:N    = \l__props_labelsep_tl ,
    itemindent        .tl_set:N    = \l__props_itemindent_tl ,
    listparindent     .tl_set:N    = \l__props_listparindent_tl ,
    labelindent       .tl_set:N    = \l__props_labelindent_tl ,
    %% Wrapper: begin/end code injected around the whole list (see
    %% \l__props_wrap_begin_tl).  Settable directly here or via a style.
    wrapper~begin     .tl_set:N    = \l__props_wrap_begin_tl ,
    wrapper~end       .tl_set:N    = \l__props_wrap_end_tl ,
    %% Unknown keys are item-level keys: route to the active item-default layer
    %% (env-local for a prop argument, cascading for \propoptions).
    unknown           .code:n      =
      {
        \exp_args:Nx \__props_defaults_append:n
          { \str_use:N \l_keys_key_str = { \exp_not:n { #1 } } }
      } ,
  }

% \cs{proplevelchoice}\marg{item1,item2,\ldots}
% picks the entry at position \cs{g__props_level_int}
% (the current \texttt{prop}/\texttt{inlineprop} nesting depth).
% If the depth exceeds the list length, the last entry is used.
% Useful in the \texttt{name} key of prop styles that should vary
% their symbol with nesting depth.
\NewExpandableDocumentCommand \proplevelchoice { m }
  {
    \clist_item:nn { #1 }
      { \int_max:nn { 1 }
        { \int_min:nn { \g__props_level_int } { \clist_count:n { #1 } } } }
  }

\NewDocumentCommand \propoptions { m }
  {
    %% \propoptions feeds the cascading layer (env-local routing off).
    \bool_set_false:N \l__props_env_arg_bool
    \keys_set:nn { props / global } { #1 }
  }

% ====================================================================
% Default global settings (set before options so user options override)
% ====================================================================

\tl_set:Nn \l__props_named_style_tl { proposition }
\tl_set:Nn \l__props_nameless_style_tl { numbered }

% ====================================================================
% Default type declarations
% ====================================================================

\SetPropStyle { plain }
  {
    format      = #1 ,
  }

\SetPropStyle { proposition }
  {
    format      = \textbf{#1} ,
  }

\SetPropStyle { thesis }
  {
    display~format = \textsc{#1} ,
    ref~format     = #1 ,
    align          = flush ,
  }

\SetPropStyle { vignette }
  {
    display~format = #1 ,
    ref~format     = \textit{#1} ,
    align          = flush ,
    label~format   = \textit{#1:} ,
  }

\SetPropStyle { bullet }
  {
    align          = center ,
    name           = \proplevelchoice {
                       \textbullet ,
                       {\normalfont \textendash} ,
                       \textasteriskcentered ,
                       \textperiodcentered
                     } ,
    display~format = #1 ,
  }

%% levelone: the standard level-1 numbered style.
\newcounter { numpropi }
\SetPropStyle { levelone }
  {
    counter     = numpropi ,
    format      = (#1) ,
  }

%% equation: uses the equation counter.
%% When the equations option is active, the equation hooks
%% (\tagform@ and \p@equation) are synced from this style's formats.
\SetPropStyle { equation }
  {
    counter        = equation ,
    format         = (#1) ,
  }

%% numbered: dispatches to the level-appropriate style via live parent.
\SetPropStyle { numbered }
  {
    style = \proplevelchoice {
              levelone , leveltwo , levelthree , levelfour , levelfive } ,
  }

%% eqnum: like numbered, but uses equation counter at level 1.
\SetPropStyle { eqnum }
  {
    style = \proplevelchoice {
              equation , leveltwo , levelthree , levelfour , levelfive } ,
  }

% ====================================================================
% Default numbered styles
% ====================================================================

% \DeclareNumberedStyle gives a style the counter of the same name, which is
% what is wanted at level 1: a document-wide sequence, reset per section.  It is
% not what is wanted deeper down, where a sublist should start again under each
% parent item.  Overriding \texttt{counter} afterwards (a later key wins) hands
% the deeper levels the shared level counters, which reset by themselves, so
% these styles can number a sublist as well as a top-level list.  The counters
% named here are created further below; nothing expands until an item uses them.

\DeclareNumberedStyle { roman }
  [
    parent         = section ,
    counter~format = \roman{#1} ,
    format         = (#1) ,
  ]
\cs_gset:Npn \theroman { \roman { roman } }
\SetPropStyle { roman }
  {
    counter = \proplevelchoice { roman , numpropii , numpropiii ,
                                 numpropiv , numpropv } ,
  }

\DeclareNumberedStyle { alph }
  [
    parent         = section ,
    counter~format = \alph{#1} ,
    display~format = #1. ,
    ref~format     = (#1) ,
  ]
\cs_gset:Npn \thealph { \alph { alph } }
\SetPropStyle { alph }
  {
    counter = \proplevelchoice { alph , numpropii , numpropiii ,
                                 numpropiv , numpropv } ,
  }

\newcounter { numpropii }
\cs_gset:Npn \thenumpropii { \alph { numpropii } }
\SetPropStyle { leveltwo }
  {
    counter        = numpropii ,
    display~format = #1. ,
    ref~format     = \parentref{#1} ,
  }

\newcounter { numpropiii }
\cs_gset:Npn \thenumpropiii { \roman { numpropiii } }
\SetPropStyle { levelthree }
  {
    counter        = numpropiii ,
    display~format = (#1) ,
    ref~format     = \parentref{.#1} ,
  }

\newcounter { numpropiv }
\cs_gset:Npn \thenumpropiv { \Alph { numpropiv } }
\SetPropStyle { levelfour }
  {
    counter        = numpropiv ,
    display~format = #1. ,
    ref~format     = \parentref{#1} ,
  }

\newcounter { numpropv }
\cs_gset:Npn \thenumpropv { \Roman { numpropv } }
\SetPropStyle { levelfive }
  {
    counter        = numpropv ,
    display~format = (#1) ,
    ref~format     = \parentref{.#1} ,
  }

%% hierarchical: 1, 1.1, 1.1.1, ... numbering using \parentref.
%% h-base handles level 1 (no parent); h-sub handles levels 2+.
\SetPropStyle { h-base }
  {
    counter        = numpropi ,
    counter~format = \arabic{#1} ,
    display~format = #1. ,
    ref~format     = #1 ,
  }

\SetPropStyle { h-sub }
  {
    counter        = \proplevelchoice {
                       numpropi , numpropii , numpropiii ,
                       numpropiv , numpropv } ,
    counter~format = \arabic{#1} ,
    format         = \parentref{.#1} ,
  }

\SetPropStyle { hierarchical }
  {
    style = \proplevelchoice { h-base , h-sub } ,
    tightspacing ,
  }

% ====================================================================
% fitmargin: left margin fitted to the label
% ====================================================================
% An environment-level style: it reads \propformlabel, the label this
% environment's items are expected to produce, which is computed once at
% \begin{prop} and is therefore only meaningful there.  Setting \leftmargin to
% that width plus \labelsep makes the body of every item line up just past the
% label, so the label sits in the hanging indent.  Use \texttt{items} when the
% items are numbered, so that the width is computed for the widest label rather
% than the first.
%
% \labelwidth must come out as \leftmargin - \labelsep, or the label box keeps
% the class default (20pt) and the label starts a box-width short of the
% margin.  Rather than say so, labelindent = 0pt says where the label box
% begins --- at the enclosing margin --- and lets the constraint resolver
% derive \labelwidth from LI + LW + LS = LM + II.  Same number, and it stays
% right if \leftmargin is overridden.
%
% align is not set.  left is the default, and right or center are reasonable
% things to want from a fitted margin: the box spans from the margin to
% \leftmargin - \labelsep whichever way the label is placed inside it.
%
% What is measured is \propwidestlabel rather than \propformlabel, so that the
% margin depends on how many digits the label has and not on which ones: a run
% of numbered environments then keeps a steady margin instead of shifting at
% every change of number.

\SetPropStyle { fitmargin }
  {
    labelindent = 0pt ,
    leftmargin  = \widthof{\propwidestlabel} + \labelsep ,
  }

% ====================================================================
% outerfit: fitmargin at the outer level only
% ====================================================================
% Meant to be set once, with \propoptions{style = outerfit}, by a document
% that wants linguex-like examples throughout.  Fitting the margin to the
% label is wanted at the outer level and unwanted below it, where a nested
% list's roman numerals or letters would drag the margin about; so each
% dimension is given a value that varies with the nesting level.
%
% A dimension key's value is resolved where it is used --- at \begin{list} for
% the list's own geometry, and again per item for the label area --- and
% \g__props_level_int is right at both points, so \proplevelchoice picks the
% entry for the level actually being set up.  The second entry is the sentinel
% *, which leaves that level exactly as it would be had the key never been set:
% class default, or free for the label-area resolver to derive.
%
% * rather than the self-assignment \setlength{\leftmargin}{\leftmargin} that
% would also leave the value alone: a self-assignment still counts as setting
% the dimension, so the resolver would treat it as protected and push any
% deficit onto another one.
%
% labelindent = 0pt rather than a labelwidth, for the reason fitmargin gives:
% it says where the label box begins and lets the resolver derive the width.
% Note that it too is dispatched by level --- 0pt at the outer level, the
% sentinel below it.  A bare 0pt would apply everywhere, pinning every nested
% list's label box to its margin, which is precisely the interference this
% style exists to avoid.
%
% The margin is the label's width plus 1.3em, \textsf{linguex}'s separation,
% rather than fitmargin's + \labelsep.  With the classes' 5pt an outer example
% reads as one run, the number almost touching its sentence and the text
% starting a good 7pt left of where an ordinary list body would; 1.3em puts it
% back at about the accustomed place while keeping the margin fitted.
% fitmargin is deliberately left alone: it is the general-purpose fitting tool,
% used for a lone named proposition as often as for numbers, and a 13pt gap
% after a bold name is an opinion it should not hold.
%
% Written into the margin rather than as labelsep = 1.3em, which would give
% the same outer level and wreck the inner ones.  \labelsep is not
% re-established per level by the standard classes the way \leftmargin and
% \labelwidth are, so a nested list inherits whatever its parent left in the
% register, and the sentinel --- which declines to assign rather than
% restoring a default --- has nothing to put back.  Nested labels then found
% themselves in a box 1.3em too narrow, overflowed it, and shoved their own
% first lines sideways.  With the width in the margin instead, labelsep is
% never touched and the deeper levels are untouched with it.  The label sits
% at the margin and the body at \leftmargin either way, so the outer level is
% indistinguishable.
%
% align is not set, for the same reason as in fitmargin, and the more so here:
% a style in force at every level should not overrule an alignment chosen
% further in.

\SetPropStyle { outerfit }
  {
    labelindent = \proplevelchoice { 0pt , * } ,
    leftmargin  =
      \proplevelchoice { \widthof{\propwidestlabel} + 1.3em , * } ,
  }

% ====================================================================
% standard: undo a cascading style's geometry
% ====================================================================
% A style can set list dimensions, spacing and wrappers, but until now nothing
% could unset them.  \__props_style_apply_dims: applies the keys a style names
% and leaves every other one alone, so asking for a different style in a prop's
% argument does not restore what an earlier \propoptions{style = ...} put in
% force: there is no clearing step for it to go through.  This style is that
% step, naming every list-level key and giving each the value that means "as if
% never set" --- which is what the * sentinel is for.
%
% Geometry only, deliberately.  Appearance cannot be reverted the same way,
% because of the order in which an item resolves: the base style chosen by
% \texttt{name} is loaded first, and the argument's keys are applied on top of
% it.  A format reset here would therefore wipe the bold of a named
% proposition rather than the cascading style's own formatting --- it cannot
% tell the two apart.  Item-level layout keys are left alone for the same
% reason; \begin{prop}[style = standard, align = left] completes the revert of
% a style, such as framed, that also set align.
%
% Keep in step with props/dims-only: a list-level key added there and not here
% will quietly survive the revert.

\SetPropStyle { standard }
  {
    topsep     = * , partopsep     = * , itemsep    = * , parsep = * ,
    leftmargin = * , rightmargin   = * , labelwidth = * , labelsep = * ,
    itemindent = * , listparindent = * , labelindent = * ,
    wrapper~begin = , wrapper~end = , continue = true ,
  }

% ====================================================================
% framed: wrap the list in a tcolorbox
% ====================================================================
% Requires \textsf{tcolorbox}.  The whole geometry lives in the style below,
% so it can be copied and adapted.  Inside the frame the list runs flush at
% \texttt{leftmargin\,=\,0}, so the contents keep the level's effective left
% margin --- read via \cs{propoperativeleftmargin} --- while the frame is
% centred with its rule one \cs{propframepad} to the left of the contents.
%
% labelindent is cleared because inside the frame the label is flush at the
% text margin, so there is no label box to indent.  Left set, an ambient
% labelindent would make the constraint resolver satisfy
% LI + LW + LS = LM + II with a positive itemindent (LM being 0 here), and
% that itemindent is exactly where a flush label lands: the whole list would
% be pushed a leftmargin's worth to the right of the frame it sits in.

\newlength \propframepad
\setlength \propframepad { 6pt }  %% padding between contents and rule (adjustable)

\msg_new:nnn { props } { no-tcolorbox }
  { Style~'framed'~needs~the~tcolorbox~package;~list~left~unframed. }

%% Definition given in ordinary catcodes so the tcolorbox keys read naturally.
\ExplSyntaxOff
\SetPropStyle{framed}{
  align = flush, leftmargin = 0pt, rightmargin = 0pt,
  labelindent = {}, continue = false,
  wrapper begin = {\begin{tcolorbox}[
      colback = white, colframe = black,
      boxrule = 0.4pt, arc = 0pt, boxsep = 0pt,
      left skip  = \dimexpr\propoperativeleftmargin-\propframepad\relax,
      right skip = \dimexpr\propoperativeleftmargin-\propframepad\relax,
      left = \propframepad, right = \propframepad,
      top  = \propframepad, bottom = \propframepad]},
  wrapper end = {\end{tcolorbox}},
}
\ExplSyntaxOn

%% Without tcolorbox, keep the flush layout but warn instead of framing.
\AtBeginDocument
  {
    \IfPackageLoadedTF { tcolorbox } { }
      {
        \SetPropStyle { framed }
          {
            wrapper~begin = { \msg_warning:nn { props } { no-tcolorbox } } ,
            wrapper~end   = { } ,
          }
      }
  }

% ====================================================================
% Package options (processed via l3keys)
% ====================================================================
% Last, after the styles exist.  The style= key applies a style's dimension
% keys as it reads them, and \__props_style_apply_dims: does nothing for a
% style it has never heard of --- so processed any earlier,
% \usepackage[style=framed] would silently produce an unframed list, the
% geometry lost and only the item-level keys surviving.
%
% Nothing between here and the top of the package reads a value an option can
% set: the defaults are established well above, and the one piece of state an
% option shares with the style definitions --- the equation hooks, which
% \SetPropStyle{equation} syncs when they are already active --- is synced
% again at \begin{document} regardless.

\ProcessKeyOptions [ props / global ]

%    \end{macrocode}
%</package>
%
% \Finale