Zulip Chat Archive

Stream: new members

Topic: How to apply function on instance of extended type


view this post on Zulip Lars Ericson (Jan 20 2021 at 18:03):

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?

view this post on Zulip Kyle Miller (Jan 20 2021 at 18:07):

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.

view this post on Zulip Kyle Miller (Jan 20 2021 at 18:08):

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

view this post on Zulip Yakov Pechersky (Jan 20 2021 at 18:08):

Also possible to provide a has_coe instance.

view this post on Zulip Lars Ericson (Jan 20 2021 at 18:11):

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


Last updated: May 13 2021 at 20:13 UTC