chore: post-leanprover#7100 cleanup (leanprover#7196)

This PR does some stage0 cleanup after leanprover#7100, and enables a warning when
the old `structure S extends P : Type` syntax is used. It also updates
the library to put resulting types in the new correct place (`structure
S : Type extends P`).

The `structure` elaborator also has some additional docstrings, and
`StructFieldKind.fromParent` is renamed to
`StructFieldKind.fromSubobject`.

doc/declarations.md

@@ -764,11 +764,12 @@ Structures and Records
 The ``structure`` command in Lean is used to define an inductive data type with a single constructor and to define its projections at the same time. The syntax is as follows:
 
 ```
-structure Foo (a : α) extends Bar, Baz : Sort u :=
+structure Foo (a : α) : Sort u extends Bar, Baz :=
 constructor :: (field₁ : β₁) ... (fieldₙ : βₙ)
 ```
 
-Here ``(a : α)`` is a telescope, that is, the parameters to the inductive definition. The name ``constructor`` followed by the double colon is optional; if it is not present, the name ``mk`` is used by default. The keyword ``extends`` followed by a list of previously defined structures is also optional; if it is present, an instance of each of these structures is included among the fields to ``Foo``, and the types ``βᵢ`` can refer to their fields as well. The output type, ``Sort u``, can be omitted, in which case Lean infers to smallest non-``Prop`` sort possible. Finally, ``(field₁ : β₁) ... (fieldₙ : βₙ)`` is a telescope relative to ``(a : α)`` and the fields in ``bar`` and ``baz``.
+Here ``(a : α)`` is a telescope, that is, the parameters to the inductive definition. The name ``constructor`` followed by the double colon is optional; if it is not present, the name ``mk`` is used by default. The keyword ``extends`` followed by a list of previously defined structures is also optional; if it is present, an instance of each of these structures is included among the fields to ``Foo``, and the types ``βᵢ`` can refer to their fields as well. The output type, ``Sort u``, can be omitted, in which case Lean infers to smallest non-``Prop`` sort possible (unless all the fields are ``Prop``, in which case it infers ``Prop``).
+Finally, ``(field₁ : β₁) ... (fieldₙ : βₙ)`` is a telescope relative to ``(a : α)`` and the fields in ``bar`` and ``baz``.
 
 The declaration above is syntactic sugar for an inductive type declaration, and so results in the addition of the following constants to the environment:
 

src/Init/Control/Basic.lean

@@ -78,7 +78,7 @@ Error recovery and state can interact subtly. For example, the implementation of
 -/
 -- NB: List instance is in mathlib. Once upstreamed, add
 -- * `List`, where `failure` is the empty list and `<|>` concatenates.
-class Alternative (f : Type u → Type v) extends Applicative f : Type (max (u+1) v) where
+class Alternative (f : Type u → Type v) : Type (max (u+1) v) extends Applicative f where
   /--
   Produces an empty collection or recoverable failure.  The `<|>` operator collects values or recovers
   from failures. See `Alternative` for more details.

src/Init/Control/Lawful/Basic.lean

@@ -47,7 +47,7 @@ pure f <*> pure x = pure (f x)
 u <*> pure y = pure (· y) <*> u
 ```
 -/
-class LawfulApplicative (f : Type u → Type v) [Applicative f] extends LawfulFunctor f : Prop where
+class LawfulApplicative (f : Type u → Type v) [Applicative f] : Prop extends LawfulFunctor f where
   seqLeft_eq  (x : f α) (y : f β)     : x <* y = const β <$> x <*> y
   seqRight_eq (x : f α) (y : f β)     : x *> y = const α id <$> x <*> y
   pure_seq    (g : α → β) (x : f α)   : pure g <*> x = g <$> x
@@ -77,7 +77,7 @@ x >>= f >>= g = x >>= (fun x => f x >>= g)
 
 `LawfulMonad.mk'` is an alternative constructor containing useful defaults for many fields.
 -/
-class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative m : Prop where
+class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplicative m where
   bind_pure_comp (f : α → β) (x : m α) : x >>= (fun a => pure (f a)) = f <$> x
   bind_map       {α β : Type u} (f : m (α → β)) (x : m α) : f >>= (. <$> x) = f <*> x
   pure_bind      (x : α) (f : α → m β) : pure x >>= f = f x

src/Init/Core.lean

@@ -2125,7 +2125,7 @@ class LeftIdentity (op : α → β → β) (o : outParam α) : Prop
 `LawfulLeftIdentify op o` indicates `o` is a verified left identity of
 `op`.
 -/
-class LawfulLeftIdentity (op : α → β → β) (o : outParam α) extends LeftIdentity op o : Prop where
+class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extends LeftIdentity op o where
   /-- Left identity `o` is an identity. -/
   left_id : ∀ a, op o a = a
 
@@ -2141,7 +2141,7 @@ class RightIdentity (op : α → β → α) (o : outParam β) : Prop
 `LawfulRightIdentify op o` indicates `o` is a verified right identity of
 `op`.
 -/
-class LawfulRightIdentity (op : α → β → α) (o : outParam β) extends RightIdentity op o : Prop where
+class LawfulRightIdentity (op : α → β → α) (o : outParam β) : Prop extends RightIdentity op o where
   /-- Right identity `o` is an identity. -/
   right_id : ∀ a, op a o = a
 
@@ -2151,13 +2151,13 @@ class LawfulRightIdentity (op : α → β → α) (o : outParam β) extends Righ
 This class does not require a proof that `o` is an identity, and is used
 primarily for inferring the identity using class resolution.
 -/
-class Identity (op : α → α → α) (o : outParam α) extends LeftIdentity op o, RightIdentity op o : Prop
+class Identity (op : α → α → α) (o : outParam α) : Prop extends LeftIdentity op o, RightIdentity op o
 
 /--
 `LawfulIdentity op o` indicates `o` is a verified left and right
 identity of `op`.
 -/
-class LawfulIdentity (op : α → α → α) (o : outParam α) extends Identity op o, LawfulLeftIdentity op o, LawfulRightIdentity op o : Prop
+class LawfulIdentity (op : α → α → α) (o : outParam α) : Prop extends Identity op o, LawfulLeftIdentity op o, LawfulRightIdentity op o
 
 /--
 `LawfulCommIdentity` can simplify defining instances of `LawfulIdentity`
@@ -2168,7 +2168,7 @@ This class is intended for simplifying defining instances of
 `LawfulIdentity` and functions needed commutative operations with
 identity should just add a `LawfulIdentity` constraint.
 -/
-class LawfulCommIdentity (op : α → α → α) (o : outParam α) [hc : Commutative op] extends LawfulIdentity op o : Prop where
+class LawfulCommIdentity (op : α → α → α) (o : outParam α) [hc : Commutative op] : Prop extends LawfulIdentity op o where
   left_id a := Eq.trans (hc.comm o a) (right_id a)
   right_id a := Eq.trans (hc.comm a o) (left_id a)
 

src/Init/Data/BEq.lean

@@ -25,7 +25,7 @@ class ReflBEq (α) [BEq α] : Prop where
   refl : (a : α) == a
 
 /-- `EquivBEq` says that the `BEq` implementation is an equivalence relation. -/
-class EquivBEq (α) [BEq α] extends PartialEquivBEq α, ReflBEq α : Prop
+class EquivBEq (α) [BEq α] : Prop extends PartialEquivBEq α, ReflBEq α
 
 @[simp]
 theorem BEq.refl [BEq α] [ReflBEq α] {a : α} : a == a :=

src/Init/Data/BitVec/Bitblast.lean

@@ -907,7 +907,7 @@ The input to the shift subtractor is a legal input to `divrem`, and we also need
 input bit to perform shift subtraction on, and thus we need `0 < wn`.
 -/
 structure DivModState.Poised {w : Nat} (args : DivModArgs w) (qr : DivModState w)
-  extends DivModState.Lawful args qr : Type where
+  extends DivModState.Lawful args qr where
   /-- Only perform a round of shift-subtract if we have dividend bits. -/
   hwn_lt : 0 < qr.wn
 

src/Init/NotationExtra.lean

@@ -307,7 +307,7 @@ syntax (name := Lean.Parser.Command.classAbbrev)
 macro_rules
   | `($mods:declModifiers class abbrev $id $params* $[: $ty]? := $[ $parents $[,]? ]*) =>
     let ctor := mkIdentFrom id <| id.raw[0].getId.modifyBase (. ++ `mk)
-    `($mods:declModifiers class $id $params* extends $[$parents:term],* $[: $ty:term]?
+    `($mods:declModifiers class $id $params* $[: $ty:term]? extends $[$parents:term],*
       attribute [instance] $ctor)
 
 macro_rules

src/Init/Prelude.lean

@@ -2865,7 +2865,7 @@ syntax over monad operations, and it depends on a `Monad` instance.
 See [the `do` notation](https://lean-lang.org/lean4/doc/do.html)
 chapter of the manual for details.
 -/
-class Monad (m : Type u → Type v) extends Applicative m, Bind m : Type (max (u+1) v) where
+class Monad (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind m where
   map      f x := bind x (Function.comp pure f)
   seq      f x := bind f fun y => Functor.map y (x ())
   seqLeft  x y := bind x fun a => bind (y ()) (fun _ => pure a)