Zulip Chat Archive

Stream: general

Topic: where


view this post on Zulip Kenny Lau (Aug 01 2020 at 06:17):

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]
-/

view this post on Zulip Kenny Lau (Aug 01 2020 at 06:18):

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

view this post on Zulip Kenny Lau (Aug 01 2020 at 06:18):

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

view this post on Zulip Kevin Buzzard (Aug 01 2020 at 06:20):

I thought that the order was random

view this post on Zulip Kenny Lau (Aug 01 2020 at 06:23):

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

Last updated: May 08 2021 at 03:17 UTC