From af30acc4dea3f32fb61b054a81e9eb0d3a5b1604 Mon Sep 17 00:00:00 2001 From: Pierre Casteran Date: Wed, 24 Jan 2024 13:50:37 +0100 Subject: [PATCH] Minor corrections --- doc/ordinal-chapter.tex | 4 ++-- theories/ordinals/OrdinalNotations/ON_Generic.v | 7 ++++--- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/doc/ordinal-chapter.tex b/doc/ordinal-chapter.tex index 268cfd99..0d4f9cf7 100644 --- a/doc/ordinal-chapter.tex +++ b/doc/ordinal-chapter.tex @@ -924,7 +924,7 @@ \subsubsection{Building an instance of \texttt{ON}} There is no interesting arithmetic on finite ordinals, since functions like successor, addition, etc., cannot be represented in \coq{} as \emph{total} functions. \end{remark} -\section{See also \dots} +\subsubsection{See also \dots} \gaiasign Finite ordinals are also formalized in \ssreflect/\mathcomp~\cite{MCB}. In Module~\href{../theories/html/gaia_hydras.ON_gfinite.html}{gaia\_hydras.ON\_gfinite}, we build an instance of class \texttt{ON}. @@ -936,7 +936,7 @@ \section{See also \dots} - See also Adam Chlipala's \emph{CPDT}~\cite{chlipalacpdt2011} for a thorough study of the use of dependent types. + diff --git a/theories/ordinals/OrdinalNotations/ON_Generic.v b/theories/ordinals/OrdinalNotations/ON_Generic.v index 47a92846..47ef853a 100644 --- a/theories/ordinals/OrdinalNotations/ON_Generic.v +++ b/theories/ordinals/OrdinalNotations/ON_Generic.v @@ -24,8 +24,9 @@ Delimit Scope ON_scope with on. Class ON {A:Type} (lt: relation A) (cmp: Compare A) := { ON_comp :> Comparable lt cmp; - ON_wf :> well_founded lt; + ON_wf : well_founded lt; }. + #[global] Existing Instance ON_comp. Coercion ON_wf : ON >-> well_founded. @@ -94,8 +95,8 @@ Class SubON { SubON_compare: forall x y : A, compareB (iota x) (iota y) = compareA x y; - SubON_incl : forall x, ltB (iota x) alpha; - SubON_onto : forall y, ltB y alpha -> exists x:A, iota x = y}. + SubON_incl : forall x, ltB (iota x) alpha; + SubON_onto : forall y, ltB y alpha -> exists x:A, iota x = y}. (* end snippet SubONDef *)