% \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}, \textsf{cleveref}, and \textsf{zref-clever}.
% \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}
%
% \begin{docCommand}{propfootnotechoice}{\marg{outside}\marg{inside}}
%   Expands to \meta{inside} within the text of a footnote, and to \meta{outside} anywhere else.  The built-in \texttt{numbered} and \texttt{eqnum} styles use it to select \texttt{footnumprop} in footnotes (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 never automatically resets, and a counter \docCounter{enumprop} which is reset at every \emph{outermost} \refEnv{prop} or \refEnv{inlineprop} environment, so that lists using this counter behave like the standard \texttt{enumerate} environment.  Finally, there is a counter \docCounter{footprop}, reset at the beginning of every footnote, used by the \texttt{footnumprop} style (see \cref{sect:styles}).
% 
% The special value \texttt{counter\,=\,none} unsets the \refKey{counter} key (potentially useful if it would otherwise have been set by a style).

% \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}
% \noindent Along with the standard commands (\cs{arabic}, \cs{roman}, \cs{Roman}, \cs{alph}, \cs{Alph}, and \cs{fnsymbol}), the following command is available:
% 
% 
% \begin{docCommand}{proprepeat}{\marg{counter}\marg{token}}
%   Prints \meta{token} as many times as the value of \meta{counter}.
% \end{docCommand}
%
% \begin{example}
% \begin{prop}[counter = enumprop, format = (#1),
%   counter format = \proprepeat{#1}{*}]
%   \item An item labelled with one asterisk.
%   \item And another, labelled with two.
% \end{prop}
% \end{example}
%
% \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.
%
% An item that continues a run in this way does not become the parent of the sub-list that follows it: the run belongs, for referring purposes, to whatever item it began under.  Taking each intervening item as the parent instead would give a run reading \texttt{1a}, \texttt{1b}, \texttt{2c}, \texttt{2d}, whose letters answer to one parent and whose prefixes to another.  This is what lets an aside between two sub-lists---the \texttt{nolabel} style of \cref{sect:builtin-styles}---interrupt a run of clauses without breaking it.  An unlabelled item that should start a fresh sub-list instead wants \texttt{[style\,=\,nolabel, reset\,=\,true]}; its sub-items then refer with no prefix, having no parent reference to inherit.
% \end{docKey}
%
% \begin{docKey}{crefname}{=\meta{type}}{no default}
%   When \textsf{cleveref} or \textsf{zref-clever} is loaded, assigns an arbitrary reference type to this proposition.  For example, \texttt{crefname=lemma} on an item for which |\ref| would produce ‘(17)’ causes \cs{cref} (\textsf{cleveref}) or \cs{zcref} (\textsf{zref-clever}) to produce ‘lemma (17)’, and \cs{Cref} or \cs{zcref}\texttt{[cap]} to produce ‘Lemma (17)’.  The \meta{type} must be known to the package in use; new types can be declared with \cs{crefname} (with \textsf{cleveref}) or \cs{zcRefTypeSetup} (with \textsf{zref-clever}).  (Bear in mind that a type carrying a format of its own will apply it to the reference this package has already formatted: \texttt{crefname=equation} turns ‘(17)’ into ‘eq.\ ((17))’, since both packages parenthesise references of that type.)
% \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,runin,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{runin} does the same but reserves no label area at all: the label becomes the first word of the item, separated from what follows by an ordinary interword space instead of a \refKey{labelsep}, so that it stretches and breaks with the rest of the line;
%   \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}.  (Note that \docValue{runin}, \docValue{nextline} and \docValue{flush-nextline} put the label into the body rather than into the label box.)
% \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[Run-in label, align=runin] Run-in aligned label, which
%       carries on as ordinary text after a single space.
%   \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}, \refKey{labelwidth}, \refKey{leftmargin}, \refKey{labelsep}, or \refKey{itemindent} can be calculated from the four others, via the expression
% \[
% \refKey{labelindent} + \refKey{labelwidth} + \refKey{labelsep} = \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 base style when an \cs{item} or \refCom{ptag} has a value for \refKey{name}.  Explicitly given keys, including \refKey{style}, will override whatever is set by this style.  
% \end{docKey}
%
% \begin{docKey}{nameless style}{=\meta{style}}{initially \texttt{numbered}}
%   The base style used when an \cs{item} or \refCom{ptag} has no value for \refKey{name}.  
% 
% The choice whether to assign an item \refKey{named style} or the \refKey{nameless style} turns on whether its \refKey{name} is set (either by its own optional argument, or by inheritance from its environment or \refCom{propoptions}).  
% \end{docKey}
%
% \begin{docKeys}[
%       doc parameter = {= \meta{style}},
%   ]
%   {
%     { doc name  = named ptag style },
%     { doc name  = nameless ptag style },
%   }
%   If set, override \refKey{named style} and \refKey{nameless style} for \refCom{ptag} items only.
% \end{docKeys}
% 
% \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 commands are provided for use with \refKey{wrapper begin} and \refKey{wrapper end}:
% \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}
%
% \begin{docCommands}{
%   { doc name = propsetabove,  doc parameter = \oarg{space above}\oarg{space below}\marg{material} },
%   { doc name = propsetbelow,  doc parameter = \oarg{space above}\oarg{space below}\marg{material} },
% }
%   For use in \refKey{wrapper begin} and \refKey{wrapper end} (respectively): sets \meta{material} in the gap above or below the list, at the list's own left margin, and vertically centred between the adjacent line of the list and the line before or after it.  The two optional arguments add vertical space on either side of it, and either may be negative.
%
% \end{docCommands}
%
% \begin{example}
% \begin{prop}[
%   wrapper begin = \propsetabove[0.2em][0.2em]{%
%     \rule{\linewidth}{0.4pt}},
%   wrapper end   = \propsetbelow[0.2em][0.2em]{%
%     \rule{\linewidth}{0.4pt}}]
%   \item A proposition bracketed by rules.
%   \item And a second one.
% \end{prop}
% \end{example}
%
% \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}).  For numbering that begins again at each list rather than running through the document, see \docCounter{enumprop} under \refKey{counter}.
% \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 and ordinary space space.
% \begin{codebox}
% \SetPropStyle{vignette}{ref format = \textit{#1},
%   align = runin, 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}
%
% \item[\texttt{nolabel}] A special style for creating items with no labels.  Also sets \refKey{reset}\,=\,\texttt{false}, so these items will not disrupt the numbering of sub-lists.
% \begin{codebox}
% \SetPropStyle{nolabel}{counter = none, name = {},
%   reset = false}
% \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}. \\
% 
%   \textit{Test:} Another line as a test.  Less space here, no?
%   \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.
%   \item[style=nolabel]
%   A proposition in style |nolabel|.  
% \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, ofr \texttt{footnumprop} if in a footnote and not nested.  
% \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{
%   \propfootnotechoice{levelone}{footnumprop},
%   leveltwo, levelthree, levelfour, levelfive}}
% \end{codebox}
%
% \item[\texttt{footnumprop}] The counter is displayed as a string of asterisks.  This style is designed to be used for numbered propositions in footnotes, which should not interrupt the numbering in the main text.  Note that the nesting
% level resets to zero inside footnotes, so a \texttt{numbered} (or
% \texttt{eqnum}) proposition immediately inside a footnote will always use
% this style.
% \begin{codebox}
% \SetPropStyle{footnumprop}{counter = footprop,
%   counter format = \proprepeat{#1}{*}, format = (#1)}
% \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{
%   \propfootnotechoice{equation}{footnumprop},
%   leveltwo, levelthree, levelfour, levelfive}}
% \end{codebox}
%
% \item[\texttt{enum}] Like |numbered| again, but at the outer level it uses
% \texttt{enumprop}, which restarts at every outermost \refEnv{prop}, so
% that the list is numbered from one however many have gone before.  This is
% the style for a one-off lists---the behaviour of \texttt{enumerate}---where
% \texttt{numbered}/\texttt{eqnum} is for numbered propositions that carry on through the document.
% \begin{codebox}
% \SetPropStyle{enumprop}{counter = enumprop, format = (#1)}
% \SetPropStyle{enum}{style = \proplevelchoice{
%   enumprop, 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}.  
% 
% \begin{prop}[style=enum]
%   \item This list will be numbered from one.
%   \item If both kinds of lists are used in the same 
%     document, they had better be formatted differently
%     so readers don't get confused.  
% \end{prop}
% \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{conclusion}] Draws a rule immediately before the list: intended to be used to display the conclusion of an argument whose premises have just been stated. 
% \begin{codebox}
% \SetPropStyle{conclusion}{wrapper begin =
%   \propsetabove[0.2em][0.2em]{\smash{\rule{\linewidth}{0.4pt}}}}
% \end{codebox}
%
% \begin{example}
% \begin{prop}[counter=enumprop, format=\textbf{P#1}]
%   \item Everything mental has physical effects.
%   \item Everything that has physical effects is physical.
% \end{prop}
% \begin{prop}[style=conclusion]
%   \item[C] Everything mental is physical.
% \end{prop}
% \end{example}
%
% \item[\texttt{standard}] 
% Resets all the environment-level keys back to their default values---potentially 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{zref-clever}, \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} or \textsf{zref-clever} loaded, all proposition items are assigned to a private |prop| ``reference type'', which by default has no special name, so |\cref| (with \textsf{cleveref}) or |\zcref| (with \textsf{zref-clever}) will generate the same output as |\ref|.  The |crefname| key can override this and set a different reference type..
%    \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}.
%
% \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.91] New \refKey{align} value \texttt{runin}, and the built-in style \texttt{vignette} changed to use it.
%
%   New style \texttt{enum} and counter \docCounter{enumprop}.
%
%   \textsf{zref-clever} is now supported alongside \textsf{cleveref}, through
%   the same \refKey{crefname} key.
%
%   New style \texttt{conclusion}, which uses new commands \refCom{propsetabove} and \refCom{propsetbelow} that
%   place material in the gap above or below a list.
%
%   New style \texttt{nolabel}, for an item with no label at all, and
%   \refKey{counter}\,=\,\texttt{none} is now documented.  An item with
%   nothing to refer to no longer takes a \refKey{ref format}: \cs{ref} to it
%   printed \texttt{()} rather than nothing.
%
%   An item carrying \refKey{reset}\,=\,\texttt{false} no longer becomes the
%   parent of the sub-list that follows it, so a run of sub-items interrupted by
%   an aside keeps the prefix it began with instead of picking up the aside's.
%   (This is a change: such sub-references used to take each intervening item as
%   their parent, giving runs like \texttt{1a}, \texttt{1b}, \texttt{2c}.)
%
%   Propositions in footnotes are numbered with asterisks by the new style
%   \texttt{footnumprop} and counter \docCounter{footprop}, and the nesting
%   level now resets inside a footnote.  New commands \refCom{proprepeat} and
%   \refCom{propfootnotechoice}.
%
%   The \texttt{prop} counter, stepped by every \refEnv{prop} and
%   \refEnv{inlineprop} but never displayed, has been withdrawn.
%
%   Stray spaces around a \refKey{name} are trimmed, so that
%   \verb|\item[ Alpha ]| places its label like \verb|\item[Alpha]|.
%
%   Equation tags hand \refKey{display format} a bare number, rather than one
%   wrapped in \textsf{amsmath}'s spacing guards.
% \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/07} {0.91}
  {Proposition labeling with key-value interface}

\RequirePackage { calc }

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

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

% --- Footnotes ---
% Whether we are inside footnote text, and the state to restore on leaving it
% (see \__props_footnote_begin:).
\bool_new:N \l__props_in_footnote_bool
\int_new:N  \l__props_saved_level_int
\bool_new:N \l__props_saved_dispmode_bool
\bool_new:N \l__props_saved_lastprop_bool
\bool_new:N \l__props_saved_topsep_bool
\tl_new:N   \l__props_saved_last_tpl_tl
\tl_new:N   \l__props_saved_last_cnt_tl
\seq_new:N  \l__props_saved_parent_tpl_seq
\seq_new:N  \l__props_saved_parent_cnt_seq

% --- 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_body_started_bool %% true when the label has already begun the item body (nextline, flush-nextline, runin)
\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
\tl_new:N   \l__props_eqtag_tl          %% equation number handed to the display format by \tagform@
%% 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} }

% ====================================================================
% \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
      }

    %% --- Trim the name ---
    %% Once, here, rather than at each place the name is formatted: it feeds
    %% both the label and the reference, so trimming at the source fixes both.
    %% l3keys already strips spaces around a key's value, which covers
    %% |name = Alpha |, but not the two routes that bypass it --- a bare name,
    %% where the whole argument is wrapped as name={...} verbatim, and a braced
    %% value, where the trimming stops at the brace.  Untrimmed, the leading
    %% space of |\item[ Alpha ]| was typeset inside the label box and pushed
    %% the label 3.8pt off the margin.  A name that genuinely wants to begin
    %% with a space can say so with ~ or \space, neither of which is trimmed.
    \tl_trim_spaces:N \l__props_name_tl

    %% --- 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 }
    %% Three alignments put the label into the body rather than into the label
    %% box --- nextline and flush-nextline end with \noindent, runin emits the
    %% label as the body's first word --- so by now the body has begun and 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.
    %% runin's separating space is emitted here rather than beside the label,
    %% so that it is the last thing on the horizontal list when the item is
    %% done.  \refstepcounter above contributes an anchor under hyperref, and
    %% an anchor between the space and here would leave \lastskip at zero: a
    %% \label in the source after \item[...] then finds \@savsk zero, so
    %% \@esphack declines to \ignorespaces, and the space that follows the
    %% \label is typeset on top of ours.  That is what put a double space
    %% after every run-in label in a document using hyperref.
    \bool_if:NT \l__props_body_started_bool
      {
        \str_if_eq:VnT \l__props_alignment_tl { runin } { \space }
        \bool_set_false:N \l__props_body_started_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
\tl_new:N \l__props_ref_tpl_tl
\tl_new:N \l__props_ref_cnt_tl

\cs_new_protected:Nn \__props_build_ref_text:
  {
    %% Build a \propapply{template}{content} token list for the aux file.
    %%
    %% An item with nothing to refer to takes no reference format, exactly as
    %% one with nothing to display takes no display format (see
    %% \cs{__props_build_item_output:}).  Otherwise \cs{ref} to an item with no
    %% label would print the format's decoration wrapped around nothing---"()"
    %% under the default nameless style---where it should print nothing.
    \tl_if_empty:NTF \l__props_ref_text_tl
      { \tl_set:Nn \l__props_ref_tpl_tl { \propfmtarg } }
      {
        \protected@edef \l__props_ref_tpl_tl
          { \l__props_reffmt:n { \propfmtarg } }
      }
    \protected@edef \l__props_ref_cnt_tl { \l__props_ref_text_tl }
    \protected@edef \l__props_ref_result_tl
      {
        \propapply
          { \exp_not:V \l__props_ref_tpl_tl }
          { \exp_not:V \l__props_ref_cnt_tl }
      }
    %% The template and content are also saved globally for \lastref and the
    %% parent stacks (pushed when entering a nested prop environment)---but not
    %% by an item carrying \texttt{reset = false}.  Such an item continues its
    %% predecessor's sub-numbering rather than starting afresh, so the sub-list
    %% that follows it belongs, for referring purposes, to whatever the run
    %% began under: taking this item as the parent would give a run reading
    %% 1a, 1b, 2c, 2d, whose letters answer to one parent and whose prefixes to
    %% another.  This is what makes an unlabelled aside usable as an intertext
    %% break in a run of clauses, \texttt{nolabel} being \texttt{reset = false};
    %% \texttt{[style = nolabel, reset = true]} is then the way to have an
    %% unlabelled item start a fresh sub-list, whose items refer with no prefix
    %% rather than inheriting one that is no longer theirs.
    \bool_if:NT \l__props_reset_bool
      {
        \tl_gset_eq:NN \g__props_last_tpl_tl \l__props_ref_tpl_tl
        \tl_gset_eq:NN \g__props_last_cnt_tl \l__props_ref_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 } }

% The same for \textsf{zref-clever}, where no such contrivance is needed: the
% \texttt{countertype} option is read when the label is set, so a local setting
% made here reaches the item's own \cs{label} exactly as \cs{@currentlabel}
% does, and is undone with the environment.
%
% \texttt{countertype}, and not \texttt{reftype}: the latter overrides the type
% of whatever label is set next, whichever counter it belongs to, and so would
% capture an equation---or anything else carrying a label---that followed the
% item inside the same list.  \texttt{countertype} is keyed to our counter, as
% the cleveref alias is.
\cs_new_protected:Nn \__props_set_zc_type:n
  { \zcsetup { countertype = { prop@anchor = #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 }
      }
    \bool_if:NT \g__props_zrefclever_bool
      {
        \tl_if_empty:NTF \l__props_crefname_tl
          { \__props_set_zc_type:n { prop } }
          { \exp_args:NV \__props_set_zc_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: } { } }
  }

% ====================================================================
% zref-clever integration
% ====================================================================

\bool_new:N \g__props_zrefclever_bool

\cs_new_protected:Nn \__props_zrefclever_setup:
  {
    \bool_gset_true:N \g__props_zrefclever_bool
    %% Map the prop@anchor counter to a private reference type "prop", for the
    %% same reason as with cleveref, and more pressingly: zref-clever ships a
    %% "proposition" type of its own, with real names, which a document may
    %% well be using for its theorems.
    \zcsetup { countertype = { prop@anchor = prop } }
    %% No name, and no separator that would leave a space where the name is
    %% not: \zcref then prints the formatted reference and nothing else, as
    %% \ref does.  namesep has to go too---an empty name alone still leaves
    %% the separator behind.
    \zcRefTypeSetup { prop }
      {
        name-sg = { } , name-pl = { } ,
        Name-sg = { } , Name-pl = { } ,
        namesep = { } ,
      }
  }

% The package hook fires at once if zref-clever is already loaded, and at its
% \cs{usepackage} otherwise, so either load order works and a document's own
% \cs{zcRefTypeSetup}\texttt{\{prop\}} always comes later and wins.  Unlike
% cleveref, nothing here has to beat a begin-document deadline: the type is
% consulted when a label is set and when \cs{zcref} runs, both of which happen
% in the document body.
\AddToHook { package/zref-clever/after } { \__props_zrefclever_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, and so
        %% reaches the format by the ordinary item path instead.
        %%
        %% amsmath writes \maketag@@@{(\ignorespaces#1\unskip\@@italiccorr)},
        %% guarding the number against stray spaces and adding an italic
        %% correction before its closing parenthesis.  We take over the
        %% parentheses, so those guards would land *inside* the format's
        %% argument and become part of #1 --- harmless to a format that prints
        %% #1, but not to one that uses it as data: \index{eq #1} then wrote
        %% the key "eq \ignorespaces 1\unskip \@@italiccorr".  Trimming the
        %% token list does the same work in the data domain, and \tag{ 5 } is
        %% still tagged 5 rather than " 5 ".
        %%
        %% The italic correction is dropped rather than moved outside, where it
        %% would sit after the closing parenthesis instead of before it.  A
        %% format wanting an italic number should say display~format =
        %% (\textit{#1}), which supplies the correction itself.
        \cs_set:Npn \tagform@ #1
          {
            \tl_set:Nn \l__props_eqtag_tl {#1}
            \tl_trim_spaces:N \l__props_eqtag_tl
            \maketag@@@
              { \exp_args:NV \__props_eqdispfmt:n \l__props_eqtag_tl }
          }
      }
  }

% ====================================================================
% 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 } }
      }
    \bool_if:NT \g__props_zrefclever_bool
      {
        %% zref-clever's amsmath module pins its notion of the current counter
        %% to \texttt{equation} for the whole of a display, and that pin
        %% outranks \cs{@currentcounter}, so the \cs{refstepcounter} below does
        %% not by itself tell zref-clever what this label belongs to: without
        %% this, a \cs{ptag} would be typed as an equation.  The setting is
        %% local, hence confined to the display, as zref-clever requires---it
        %% is not undone by a later \cs{refstepcounter} the way
        %% \cs{@currentcounter} is.
        \zcsetup { currentcounter = prop@anchor }
        \tl_if_empty:nTF { #2 }
          { \__props_set_zc_type:n { prop } }
          { \__props_set_zc_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: [ ] }
      {
        %% The three alignments that put the label into the body rather than
        %% into the label box.  They are settled before the per-item dimension
        %% question below, since a label that never enters the box cannot be
        %% positioned by the dimensions that size it.
        \bool_lazy_any:nTF
          {
            { \str_if_eq_p:Vn \l__props_alignment_tl { nextline } }
            { \str_if_eq_p:Vn \l__props_alignment_tl { flush-nextline } }
            { \str_if_eq_p:Vn \l__props_alignment_tl { runin } }
          }
          { \__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_body_started_bool
      }
      {
        \str_if_eq:VnTF \l__props_alignment_tl { runin }
          {
            %% Label as the first word of the body, separated from what
            %% follows by an ordinary interword space rather than \labelsep.
            %% Like flush, but without reserving the label area: the list item
            %% is opened with no label at all and the label is simply the text
            %% the body starts with, so it wraps and stretches with the rest of
            %% the line.
            %% The separating space is not emitted here but at the end of
            %% \__props_item_cmd:, after the cross-referencing machinery: see
            %% the note there.
            \__props_list_item: []
            \l__props_item_output_tl
            \bool_set_true:N \l__props_body_started_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_body_started_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 } }
  }

% ====================================================================
% \cs{propsetabove} / \cs{propsetbelow} --- material set in the gap
% ====================================================================
% Set the material in the gap above (below) the list: at the list's own left
% margin, vertically centred between the text on either side.  The material's
% own height and depth add to the gap, as they would anywhere else, so a rule
% that should cost nothing is smashed by the caller.
%
% Four things have to be got right, none of them the caller's business.
%
% The material must not disturb the seamless join (see \texttt{continue}),
% which works by depositing the join glue and setting \cs{topsep} to match, so
% that \cs{@trivlist}'s \cs{addvspace} finds \cs{lastskip} already equal to it
% and adds nothing.  A box appended after that glue makes \cs{lastskip} zero
% and the join is laid down a second time.  So the material is slipped inside
% the glue: step back over it, drop the material in, put it back.
% \cs{prevdepth} is restored with it, so the line spacing on either side is
% what it would have been.
%
% The gap to bisect is the join glue when the lists are joining---including
% when that glue is zero, which is what \texttt{itemsep\,=\,0pt} asks for---and
% the list's own \cs{topsep}+\cs{partopsep} when they are not.  Reading
% \cs{lastskip}\,>\,0pt as ``is there a join'' mistakes the former for the
% latter, and puts the rule through the following line.
%
% Inside an enclosing list, the paragraph break lets the outer list add its
% \cs{parsep} as well; that glue lands after our insertion point, where
% \cs{lastskip} cannot see it.
%
% The gap is bounded by ink---descenders on one side, capitals on the
% other---and ink is sized by the font, not by the leading.  Under
% \textsf{setspace}'s \cs{doublespacing} the strut grows with
% \cs{baselineskip} while the letters stay put, so a strut-based calculation
% drifts up the page.
\skip_new:N \l__props_gap_join_skip     %% the glue there, to be put back
\dim_new:N  \l__props_gap_depth_dim     %% depth of the line above, if any
\dim_new:N  \l__props_gap_saved_dp_dim  %% \prevdepth exactly as found, to restore
\dim_new:N  \l__props_gap_sep_dim       %% what separates the two baselines
\dim_new:N  \l__props_gap_cap_dim       %% height of a capital in this font
\dim_new:N  \l__props_gap_drop_dim      %% how far to lower the material
\box_new:N  \l__props_gap_box
\box_new:N  \l__props_gap_out_box
\dim_new:N  \l__props_gap_half_dim      %% half the gap the material sits in
\dim_new:N  \l__props_gap_clear_dim     %% clearance to create when nothing is above
\bool_new:N \l__props_gap_atop_bool     %% nothing above: top of a page or box

\cs_new_protected:Nn \__props_gap_start:
  {
    \par
    \skip_set:Nn \l__props_gap_join_skip { \lastskip }
    \dim_set:Nn  \l__props_gap_saved_dp_dim { \prevdepth }
    \dim_set:Nn  \l__props_gap_cap_dim      { \fontcharht \font `X }
    %% At the top of a page or a box there is no line above and \prevdepth
    %% holds TeX's -1000pt sentinel, which would throw the material half a
    %% metre down the page.  Nothing precedes, so nothing descends: take the
    %% depth as zero for the arithmetic, but restore the sentinel afterwards,
    %% since it is also what tells TeX to add no glue above the first line.
    \dim_set_eq:NN \l__props_gap_depth_dim \l__props_gap_saved_dp_dim
    \bool_set_false:N \l__props_gap_atop_bool
    \dim_compare:nNnT { \l__props_gap_depth_dim } < { -500pt }
      {
        \bool_set_true:N \l__props_gap_atop_bool
        \dim_zero:N \l__props_gap_depth_dim
      }
  }

%% \l__props_gap_sep_dim has been set by the caller.
%% #1 = space above, #2 = space below, #3 = material.
\cs_new_protected:Npn \__props_gap_place:nnn #1#2#3
  {
    \hbox_set:Nn \l__props_gap_box {#3}
    %% A box contributed in vertical mode has its *top* at the current
    %% position, so its height is space above the material and its depth
    %% space below it: the two arguments are simply added to them.  A rule
    %% laid into a gap consumes the white that marks the division, so a rule
    %% given no space reads tighter than the plain gap between two items ---
    %% the opposite of what it is there to say.
    \box_set_ht:Nn \l__props_gap_box { \box_ht:N \l__props_gap_box + #1 }
    \box_set_dp:Nn \l__props_gap_box { \box_dp:N \l__props_gap_box + #2 }
    \dim_compare:nNnT { \@totalleftmargin } > { 0pt }
      { \dim_add:Nn \l__props_gap_sep_dim { \parsep } }
    %% Half the gap, measured between the ink on either side: the descenders
    %% above and the capitals below.  The material's own size does not enter
    %% into it --- whatever it is, it ends up with this much white on each
    %% side, plus whatever the two arguments asked for.
    \dim_set:Nn \l__props_gap_half_dim
      {
        (
          \baselineskip + \l__props_gap_sep_dim
          - \l__props_gap_depth_dim - \l__props_gap_cap_dim
        ) / 2
      }
    %% With nothing above, there is no gap to sit in: TeX discards the glue at
    %% the top of a page or box, so the list begins flush against it.  The
    %% material goes at the top, and the clearance it would have had lower
    %% down the page is created below it instead, as depth on the box.  (A
    %% page break between the premises and their conclusion lands here.)
    \bool_if:NTF \l__props_gap_atop_bool
      {
        \dim_zero:N \l__props_gap_drop_dim
        \dim_set_eq:NN \l__props_gap_clear_dim \l__props_gap_half_dim
        \dim_compare:nNnT { \l__props_gap_clear_dim } < { 0pt }
          { \dim_zero:N \l__props_gap_clear_dim }
      }
      {
        \dim_set_eq:NN \l__props_gap_drop_dim \l__props_gap_half_dim
        \dim_zero:N \l__props_gap_clear_dim
      }
    \vskip -\l__props_gap_join_skip
    \nointerlineskip
    %% \parshape indents paragraphs, not boxes: a box contributed in vertical
    %% mode inside a list would sit at the page margin, not the list's.
    \hbox_set:Nn \l__props_gap_out_box
      {
        \skip_horizontal:n { \@totalleftmargin }
        \box_move_down:nn { \l__props_gap_drop_dim }
          { \box_use:N \l__props_gap_box }
      }
    %% The box keeps the height and depth of the padded material---that much
    %% space it does cost---but not the displacement, and no width.
    \box_set_ht:Nn \l__props_gap_out_box { \box_ht:N \l__props_gap_box }
    \box_set_dp:Nn \l__props_gap_out_box
      { \box_dp:N \l__props_gap_box + \l__props_gap_clear_dim }
    \box_set_wd:Nn \l__props_gap_out_box { \c_zero_dim }
    \box_use:N \l__props_gap_out_box
    \prevdepth \l__props_gap_saved_dp_dim
    \nobreak
    \vskip \l__props_gap_join_skip
  }

\NewDocumentCommand \propsetabove { O{0pt} O{0pt} m }
  {
    \group_begin:
      \__props_gap_start:
      \bool_if:NTF \g__props_suppress_topsep_bool
        { \dim_set:Nn \l__props_gap_sep_dim { \l__props_gap_join_skip } }
        { \dim_set:Nn \l__props_gap_sep_dim { \topsep + \partopsep } }
      \__props_gap_place:nnn {#1} {#2} {#3}
    \group_end:
  }

\NewDocumentCommand \propsetbelow { O{0pt} O{0pt} m }
  {
    \group_begin:
      \__props_gap_start:
      %% Below the list, the glue \endtrivlist has just added is the gap.
      \dim_set:Nn \l__props_gap_sep_dim { \l__props_gap_join_skip }
      \__props_gap_place:nnn {#1} {#2} {#3}
    \group_end:
  }

% ====================================================================
% 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{} }
  {
    \int_gincr:N \g__props_level_int
    %% enumprop restarts at every outermost environment, so that a list using
    %% it numbers from one each time, the way enumerate does.  Reset here
    %% rather than at \end, so that it is right even if the document leaves an
    %% environment by some other route.
    \int_compare:nNnT { \g__props_level_int } = { 1 }
      { \setcounter { enumprop } { 0 } }
    %% 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{} }
  {
    \int_gincr:N \g__props_level_int
    %% enumprop restarts at every outermost environment, so that a list using
    %% it numbers from one each time, the way enumerate does.  Reset here
    %% rather than at \end, so that it is right even if the document leaves an
    %% environment by some other route.
    \int_compare:nNnT { \g__props_level_int } = { 1 }
      { \setcounter { enumprop } { 0 } }
    %% 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 } } } }
  }

% \cs{propfootnotechoice}\marg{outside}\marg{inside}
% expands to the second argument inside footnote text and the first
% elsewhere.  Expandable, so that it can stand where a style name or a
% counter name is wanted.
\NewExpandableDocumentCommand \propfootnotechoice { m m }
  { \bool_if:NTF \l__props_in_footnote_bool { #2 } { #1 } }

% \cs{proprepeat}\marg{counter}\marg{token} prints \meta{token} as many times
% as the value of \meta{counter}: the counter format behind (*), (**), (***).
% Expandable, since a counter format is expanded as the item resolves.
\NewExpandableDocumentCommand \proprepeat { m m }
  { \prg_replicate:nn { \value {#1} } {#2} }

% --- Footnote text ---
%
% Two things happen on entering footnote text.
%
% The footprop counter is restarted, so that each footnote numbers from one.
% (Declaring the counter within \texttt{footnote} would reset it when the mark
% is placed rather than when the text is set, and would miss \texttt{minipage}
% footnotes, which count with \texttt{mpfootnote}.)
%
% The nesting level is zeroed, so that a prop inside a footnote hanging from a
% prop starts afresh instead of nesting inside the item it hangs from.
%
% Everything else that records where we are in the prop structure is saved and
% restored with it.  All of it is global by necessity---it has to survive the
% prop environment's own group---so the group around footnote text will not
% restore it; and footnote text is set out of order with respect to the
% structure it interrupts, so none of what happens inside it should be visible
% to the list it hangs from.  Restoring the level alone is not enough: a prop
% closing at level 1 inside the footnote would take \g__props_display_mode_bool
% global false, and the item after the footnote would then be set inline,
% running on from the item before it.  The saved values are local, so nested
% boxes unwind by themselves.
%
% Patching \cs{@footnotetext} directly, as \textsf{linguex} does, would clash
% with any other package that patches it (\textsf{setspace}, for one).  The
% generic command hooks are applied at \cs{begin}\texttt{\{document\}}, and so
% land on whatever definition is finally in force.
\cs_new_protected:Nn \__props_footnote_begin:
  {
    \bool_set_true:N \l__props_in_footnote_bool
    \int_set_eq:NN  \l__props_saved_level_int      \g__props_level_int
    \bool_set_eq:NN \l__props_saved_dispmode_bool  \g__props_display_mode_bool
    \bool_set_eq:NN \l__props_saved_lastprop_bool  \g__props_last_was_prop_bool
    \bool_set_eq:NN \l__props_saved_topsep_bool    \g__props_suppress_topsep_bool
    \tl_set_eq:NN   \l__props_saved_last_tpl_tl    \g__props_last_tpl_tl
    \tl_set_eq:NN   \l__props_saved_last_cnt_tl    \g__props_last_cnt_tl
    \seq_set_eq:NN  \l__props_saved_parent_tpl_seq \g__props_parent_tpl_seq
    \seq_set_eq:NN  \l__props_saved_parent_cnt_seq \g__props_parent_cnt_seq
    \int_gzero:N        \g__props_level_int
    \bool_gset_false:N  \g__props_display_mode_bool
    \bool_gset_false:N  \g__props_last_was_prop_bool
    \setcounter { footprop } { 0 }
  }
\cs_new_protected:Nn \__props_footnote_end:
  {
    \bool_set_false:N \l__props_in_footnote_bool
    \int_gset_eq:NN  \g__props_level_int            \l__props_saved_level_int
    \bool_gset_eq:NN \g__props_display_mode_bool    \l__props_saved_dispmode_bool
    \bool_gset_eq:NN \g__props_last_was_prop_bool   \l__props_saved_lastprop_bool
    \bool_gset_eq:NN \g__props_suppress_topsep_bool \l__props_saved_topsep_bool
    \tl_gset_eq:NN   \g__props_last_tpl_tl          \l__props_saved_last_tpl_tl
    \tl_gset_eq:NN   \g__props_last_cnt_tl          \l__props_saved_last_cnt_tl
    \seq_gset_eq:NN  \g__props_parent_tpl_seq       \l__props_saved_parent_tpl_seq
    \seq_gset_eq:NN  \g__props_parent_cnt_seq       \l__props_saved_parent_cnt_seq
  }
\AddToHook { cmd/@footnotetext/before }   { \__props_footnote_begin: }
\AddToHook { cmd/@footnotetext/after }    { \__props_footnote_end: }
\AddToHook { cmd/@mpfootnotetext/before } { \__props_footnote_begin: }
\AddToHook { cmd/@mpfootnotetext/after }  { \__props_footnote_end: }

\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          = runin ,
    label~format   = \textit{#1:} ,
  }

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

%% nolabel: an item with no label at all.  counter=none alone suppresses the
%% counter but not a name, so it leaves the label standing when one is
%% inherited from the environment or supplied by a style (bullet, say); as a
%% style, this displaces the name too.  reset=false because such an item is
%% typically an aside in the middle of a list, after which a sub-list should
%% carry on from where the last one left off rather than start again.
\SetPropStyle { nolabel }
  {
    counter = none ,
    name    = { } ,
    reset   = false ,
  }

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

%% enumprop: like numpropi, but restarted at every outermost prop or
%% inlineprop environment (see those environments), so that a list numbers
%% from one each time it is used, as enumerate does.  numpropi runs on through
%% the document instead, which is what one wants for propositions that are
%% referred to from elsewhere, and not what one wants for a one-off list.
\newcounter { enumprop }
\SetPropStyle { enumprop }
  {
    counter     = enumprop ,
    format      = (#1) ,
  }

%% footnumprop: for items inside footnote text, where the document's numbering
%% would be an intrusion.  Asterisks, after the fashion of linguex and philex.
%% Restarted at every footnote (see \__props_footnote_begin:).
\newcounter { footprop }
\SetPropStyle { footnumprop }
  {
    counter        = footprop ,
    counter~format = \proprepeat {#1} {*} ,
    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.
%% The level-1 entry branches on footnote text, so that a footnote does not
%% consume a document number.  Branching here rather than inside levelone
%% keeps the behaviour when a document redefines levelone.  Deeper levels do
%% not branch: the level is zeroed on entering a footnote, so anything deeper
%% than 1 there is a sublist of the footnote's own outer item.
\SetPropStyle { numbered }
  {
    style = \proplevelchoice {
              \propfootnotechoice { levelone } { footnumprop } ,
              leveltwo , levelthree , levelfour , levelfive } ,
  }

%% enum: like numbered, but uses the restarting enumprop counter at level 1.
\SetPropStyle { enum }
  {
    style = \proplevelchoice {
              enumprop , leveltwo , levelthree , levelfour , levelfive } ,
  }

%% eqnum: like numbered, but uses equation counter at level 1.
\SetPropStyle { eqnum }
  {
    style = \proplevelchoice {
              \propfootnotechoice { equation } { footnumprop } ,
              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   = { } ,
          }
      }
  }

%% conclusion: a rule across the text width, immediately above the list, for
%% the conclusion of an argument whose premises are in the list before it.
%% Smashed, so that the rule costs no vertical space and the first item sits
%% exactly where it would have without it.  The 0.2em of space on each side
%% follows bussproofs and ebproof, which both give an inference line 2pt.
\SetPropStyle { conclusion }
  {
    wrapper~begin = \propsetabove [0.2em] [0.2em]
                      { \smash { \rule { \linewidth } { 0.4pt } } } ,
  }

% ====================================================================
% 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