Invalid type ascription??

Stream: general

[Neil Strickland]

I am mystified by this:

def foo (a : ℕ) : fin a.succ := begin
 let z : fin a.succ := 0,
 let q : ℕ → (fin a.succ) := λ b, z,
 exact z
end

After the definition of q, I get

invalid type ascription, term has type
  ℕ → fin (nat.succ a)
but is expected to have type
  Π (a : ℕ), fin (nat.succ a)
state:
a : ℕ,
z : fin (nat.succ a) := 0
⊢ fin (nat.succ a)

So q has the type that I said it should have, but for some reason Lean expects it to have a different type?

[Reid Barton]

You have stumbled across a highly dubious Lean feature.

[Reid Barton]

In tactic mode (only), q : ℕ → (fin a.succ) means q : Π (a : ℕ), (fin a.succ).

[Reid Barton]

In other words → is expanded to a Pi type using the fixed variable name a.

[Mario Carneiro]

'''''''''''feature'''''''''''

[Neil Strickland]

Thanks. So I see that this works instead:

def foo (a : ℕ) : fin a.succ := begin
 let z : fin a.succ := 0,
 let q : ∀ b : ℕ, (fin a.succ) := λ b, z,
 exact z
end

[Kevin Buzzard]

What did I tell you about making definitions using tactic mode Neil??

[Kevin Buzzard]

[PS I was doing this myself earlier today :-)]