How to apply function on instance of extended type

Stream: new members

[Lars Ericson]

The last line doesn't work:

import data.int.basic

structure intpt :=
(x : int) (y: int)

structure pos_point extends intpt :=
(pos : x > 0)

def f (pt: intpt) := pt.x+1

variable p: pos_point

def g (p: pos_point) := f(p)

The error is

type mismatch at application
  f p
term
  p
has type
  pos_point
but is expected to have type
  intpt

but p is an instance of an extension of pos_point. What's the right way to apply f inside of g?

[Kyle Miller]

Lean doesn't automatically cast things to super-structures for you -- you need to do f p.to_intpt. The extends keyword's function is to define these "projection functions" and make it so you can use the super-structure's fields in the sub-structure.

[Kyle Miller]

(and p.to_intpt is syntactic sugar for pos_point.to_intpt p)

[Yakov Pechersky]

Also possible to provide a has_coe instance.

[Lars Ericson]

Thanks, I forgot that extends auto-generates the casts.