From 1292819f642632c097f84caed9c0818477bbb28e Mon Sep 17 00:00:00 2001
From: Denis Gorbachev <829578+DenisGorbachev@users.noreply.github.com>
Date: Sat, 10 Jun 2023 14:55:55 +0700
Subject: [PATCH] chore: update scripts example to new `GetElem` syntax
 (leanprover/lake#171)

---
 README.md                      | 2 +-
 examples/scripts/lakefile.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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