where

Stream: general

[Kenny Lau]

import ring_theory.algebra

variables {R A : Type*} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A)
#where

/-
namespace [root namespace]

variables {R : Type u_1} {A : Type u_2} (S : subalgebra R A) [comm_semiring R] [semiring A] [algebra R A]



end [root namespace]
-/

[Kenny Lau]

the printed combination is impossible because S : subalgebra R A depends on algebra R A

[Kenny Lau]

is this intentional (to print all the instances last)?

[Kevin Buzzard]

I thought that the order was random

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/37ab4263b452f08180e2a08f0020b7bc6cf08676/src/tactic/where.lean#L25-L31

/-- Assigns a priority to each binder for determining the order in which variables are traced. -/
meta def binder_priority : binder_info → ℕ
| binder_info.implicit := 1
| binder_info.strict_implicit := 2
| binder_info.default := 3
| binder_info.inst_implicit := 4
| binder_info.aux_decl := 5