diff --git a/README.md b/README.md
index 7da1e70467..8c138a0034 100644
--- a/README.md
+++ b/README.md
@@ -319,7 +319,7 @@ Greet the entity with the given name. Otherwise, greet the whole world.
 -/
 script greet (args) do
   if h : 0 < args.length then
-    IO.println s!"Hello, {args.get 0 h}!"
+    IO.println s!"Hello, {args[0]'h}!"
   else
     IO.println "Hello, world!"
   return 0
diff --git a/examples/scripts/lakefile.lean b/examples/scripts/lakefile.lean
index 5d292e08fa..9552d46561 100644
--- a/examples/scripts/lakefile.lean
+++ b/examples/scripts/lakefile.lean
@@ -14,7 +14,7 @@ Greet the entity with the given name. Otherwise, greet the whole world.
 @[default_script]
 script greet (args) do
   if h : 0 < args.length then
-    IO.println s!"Hello, {args.get ⟨0, h⟩}!"
+    IO.println s!"Hello, {args[0]'h}!"
   else
     IO.println "Hello, world!"
   return 0