Zulip Chat Archive

Stream: lean4

Topic: abbreviation issue


view this post on Zulip Hossam Karim (Jan 26 2021 at 18:43):

I am very new to lean, not sure why this doesn't type check, the last line has the issue. Not sure if the abbrev syntax means what I assumed also.

structure DepFn (α : Type) where
  β : Type
  apply : α  β

def ap (f: DepFn α) : α  f.β := f.apply -- type checks

abbrev DepFnL (αα  ββ : Type) := DepFn αα where
  β := ββ

def lifted : DepFnL String String := String, id -- type checks
-- def lifted : DepFnL String String := (⟨String, id⟩ : DepFn String) -- also type checks

-- type mismatch f.apply has type α → f.β but is expected to have type α → β
def apL : DepFnL α β  α  β := λ f => f.apply -- ****issue here****

view this post on Zulip Reid Barton (Jan 26 2021 at 18:48):

I'm not sure what you wanted abbrev DepFnL (αα ββ : Type) := DepFn αα where β := ββ to do, but it doesn't do it. The where clause does nothing because β isn't used, so it's the same as abbrev DepFnL (αα ββ : Type) := DepFn αα.

view this post on Zulip Reid Barton (Jan 26 2021 at 18:50):

I guess you wanted to say something like DepFnL αα ββ is the the type of DepFn ααs whose β field is (by definition) ββ. But this feature doesn't exist in Lean.

view this post on Zulip Hossam Karim (Jan 26 2021 at 18:52):

Yes, exactly, that's what I wanted to do. I expected some kind of type refinement or restriction, but it doesn't seem to be designed this way. Thanks a lot.

view this post on Zulip Hossam Karim (Jan 26 2021 at 18:53):

Wondering why the where expression is allowed then?

view this post on Zulip Reid Barton (Jan 26 2021 at 18:53):

where is another way to write let, I think (from Haskell)

view this post on Zulip Hossam Karim (Jan 26 2021 at 18:54):

Understood, I wonder what can I do with it in the context of an abbrev

view this post on Zulip Reid Barton (Jan 26 2021 at 18:59):

Another possible source of confusion is that there is another form
def foo where ... (no :=)
which is basically the same as
def foo := { ... }

view this post on Zulip Nick Chopper (Jan 28 2021 at 07:02):

one of

@DepFn.mk αα ββ

or

structure DepFn' (α : Type) (β : Type) where
  apply : α  β

maybe what you want)


Last updated: May 07 2021 at 13:21 UTC