Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Aug 08 2020 at 05:50):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Aug 08 2020 at 05:52):

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

view this post on Zulip 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!

view this post on Zulip Kenny Lau (Aug 08 2020 at 06:26):

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

view this post on Zulip Kenny Lau (Aug 08 2020 at 06:36):

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

view this post on Zulip Kenny Lau (Aug 08 2020 at 06:36):

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

view this post on Zulip Scott Morrison (Aug 08 2020 at 06:40):

I was wondering about the same thing!

view this post on Zulip Kenny Lau (Aug 08 2020 at 06:41):

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

view this post on Zulip 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