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
The following code typechecks with Lean 4.9.1, but not with 4.10.1-rc1 and later:
structureAsdf: Type u where
deffoo (T: Type u) : Asdf.{u} := {}
defbar
(T: Type u)
(holdsForAll: ∀ n: Asdf, True)
:
True
:=
let n := foo T
holdsForAll n
The error:
application type mismatch
holdsForAll n
argument
n
has type
Asdf : Type u
but is expected to have type
Asdf : Type u_1
An easy workaround is to propagate the universe explicitly:
(holdsForAll: ∀ n: Asdf.{u}, True)
Expected behavior: The code produces no errors.
Versions
Lean versions affected: 4.10.0-rc1, lean nightly as of wriging
OS: Ubuntu 22.04.4 LTS
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
The following code typechecks with Lean 4.9.1, but not with 4.10.1-rc1 and later:
The error:
An easy workaround is to propagate the universe explicitly:
Expected behavior: The code produces no errors.
Versions
Lean versions affected: 4.10.0-rc1, lean nightly as of wriging
OS: Ubuntu 22.04.4 LTS
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: