Using dot notation on type aliases

Stream: new members

[Philipp]

I want to define a type Pos storing x and y coordinates. To keep things simple I just use def Pos := Int × Int.

I can then define functions like

def Pos.valid (pos : Pos) : Bool :=
  pos.1 ≥ 0 && pos.2 ≥ 0

But how can I call them?

#eval (0,1).isValid
#eval ((0,1) : Pos).isValid

Results in

invalid field 'isValid', the environment does not contain 'Prod.isValid'
  (0, 1)
has type
  ?m.6156 × ?m.6164

It works if I introduce a let:

#eval let (p : Pos) := ((0:Int),(1:Int))
p.valid

but that's not very convenient.

[Philipp]

Also, why would Pos not be inhabited? Am I using type aliases completely wrong?

[Yaël Dillies]

Yes. Type aliases forget a lot of things about the original type.

[Yaël Dillies]

For one, if you want to copy over an existing instance, you should use a deriving clause:

def Pos := Int × Int
deriving Inhabited

[Kyle Miller]

If you use abbrev Pos instead of def Pos then all instances and dot notation carry over