You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
include now refuses to include strict implicit section variables.
Context
I ran into this on Mathlib's nightly-testing branch moving to nightly-2024-08-22 , in Mathlib/Analysis/Complex/TaylorSeries.lean.
Steps to Reproduce
section
variable {i : Nat}
include i in -- Works
example : True := by
have _ := i
trivial
end
section
variable ⦃i : Nat⦄
include i in -- Fails with "invalid 'include', variable 'i' has not been declared in the current scope"
example : True := by
have _ := i
trivial
end
Versions
nightly-2024-08-22, was working fine on nightly-2024-08-21
Description
include
now refuses to include strict implicit section variables.Context
I ran into this on Mathlib's nightly-testing branch moving to
nightly-2024-08-22
, inMathlib/Analysis/Complex/TaylorSeries.lean
.Steps to Reproduce
Versions
nightly-2024-08-22
, was working fine onnightly-2024-08-21
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: