difference between \Pi{X:Type} and ?M_1

Stream: new members

[Chris M]

I have the following:

variable {Z:Type}
def g: Z → Z := sorry
#check (g:Π {Z:Type}, Z → Z)

Which gives the following error:

invalid type ascription, term has type
  ?m_1 → ?m_1 : Type
but is expected to have type
  Π {Z : Type}, Z → Z : Type 1

I was under the impression that these are the same thing, or at least that variable {Z:Type} def g: Z → Z := sorry can be thought of as g:Π {Z:Type}, Z → Z. What is the difference?

[Yury G. Kudryashov]

Once you define

def g {Z : Type} (x : Z) := x

the function g has type ?m_1 → ?m_1. It means that it will not look for an argument of type Type.

[Yury G. Kudryashov]

You can use @g to be able to set implicit arguments.

[Yury G. Kudryashov]

There is also a version

def g {{Z : Type}} (x : Z) := x

With this definition g has type Π {{Z : Type}} (x : Z), Z while g x, x : Z has type Z.

[Yury G. Kudryashov]

I.e., lean does not process the argument in {{ }} unless you provide more explicit arguments.

[Scott Morrison]

If you just write g, Lean feeds it metavariables to fill in the implicit arguments. So it's now a function ?m_1 → ?m_1, as Yury says. This distinction between "a function with an implicit argument, not yet applied" and "a function applied to a metavariable" is a bit subtle!

[Kenny Lau]

why do we use {} instead of {{}}?

[Kenny Lau]

I think ⦃⦄ works much better than {} but perhaps it takes a bit more keystrokes

[Kenny Lau]

I think ⦃⦄ is so preferable that it should replace {} as the default behaviour

[Scott Morrison]

I was wondering about the same thing!

[Kenny Lau]

what if I were to make a PR that replaces all {} to ⦃⦄

[Scott Morrison]

It might be cheaper to try out a change to core that swaps their meanings??