diff --git a/doc/lean3changes.md b/doc/lean3changes.md index 3ad28c51ff..672dbc3eec 100644 --- a/doc/lean3changes.md +++ b/doc/lean3changes.md @@ -25,7 +25,9 @@ def Prod.str : Nat × Nat → String := fun (a, b) => "(" ++ toString a ++ ", " ++ toString b ++ ")" structure Point where - x y z : Nat + x : Nat + y : Nat + z : Nat def Point.addX : Point → Point → Nat := fun { x := a, .. } { x := b, .. } => a+b