From caa3136558a88baa992e095cfe3d2216cbfb5c35 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Dec 2020 09:41:42 -0800
Subject: [PATCH] fix: doc

---
 doc/lean3changes.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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