構造体と名前空間とドット記法

これって、昔Catyでやろうとしていたこと（一部はやった）ことだ。

structure LatticePoint2D where
  x: Int
  y: Int
#check LatticePoint2D

def LatticePoint2D.moveBy (p : LatticePoint2D) (u v:Int)  : LatticePoint2D :=
  { 
    x := p.x + u
    y := p.y + v
  }
#check LatticePoint2D.moveBy

#check ({x:=0, y:=3} : LatticePoint2D)
#check LatticePoint2D.moveBy {x:=0, y:=3} 3 2
#eval LatticePoint2D.moveBy {x:=0, y:=3} 3 2 -- エラー：プリントできない
#check ({x:=0, y:=3} : LatticePoint2D).moveBy 2 3 -- OK