chore: update scripts example to new GetElem syntax (leanprover/lake#171)

This commit is contained in:
Denis Gorbachev 2023-06-10 14:55:55 +07:00 committed by GitHub
parent 3fb146fad2
commit 1292819f64
2 changed files with 2 additions and 2 deletions

View file

@ -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

View file

@ -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