blob: 73ea2a3cf897835bbe29d5d1e4bb8594a2b33b6c [file] [edit]
def f (y : Nat) :=
let x := 1x + y -- Error
structure Point where
x : Nat
y : Nat
deriving Repr
def mkPoint1 (a : Nat) : Point where
x := 1y := a -- Error
def mkPoint2 (a : Nat) : Point where
x := 1
y := a
def mkPoint3 (a : Nat) : Point where
x := 1; y := a
def mkPoint?? (x y : Nat) : Point :=
{ x y }