abbreviation issue

Stream: lean4

[Hossam Karim]

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****

[Reid Barton]

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 αα.

[Reid Barton]

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.

[Hossam Karim]

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.

[Hossam Karim]

Wondering why the where expression is allowed then?

[Reid Barton]

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

[Hossam Karim]

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

[Reid Barton]

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

[Nick Chopper]

one of

@DepFn.mk αα ββ

or

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

maybe what you want)