Stream: new members

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

Chris M (Aug 08 2020 at 04:14):

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 (Aug 08 2020 at 05:50):

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 (Aug 08 2020 at 05:50):

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

Yury G. Kudryashov (Aug 08 2020 at 05:51):

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 (Aug 08 2020 at 05:52):

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

Scott Morrison (Aug 08 2020 at 05:55):

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 (Aug 08 2020 at 06:26):

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

Kenny Lau (Aug 08 2020 at 06:36):

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

Kenny Lau (Aug 08 2020 at 06:36):

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

Scott Morrison (Aug 08 2020 at 06:40):

I was wondering about the same thing!

Kenny Lau (Aug 08 2020 at 06:41):

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

Scott Morrison (Aug 08 2020 at 06:55):

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

Last updated: May 13 2021 at 06:15 UTC