Fix copy-paste mistake

Fixes #37
leanprover · Jul 17, 2022 · 0a6ebbe · 0a6ebbe
1 parent 36a7b06
commit 0a6ebbe
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/functional-programming-lean/src/getting-to-know/conveniences.md b/functional-programming-lean/src/getting-to-know/conveniences.md
@@ -391,9 +391,9 @@ For instance, `{{#example_in Examples/Intro.lean pointPosEvalNoType}}` yields th
 {{#example_out Examples/Intro.lean pointPosEvalNoType}}
 ```
 The metavariable in the error is because there is no type information available.
-Adding an annotation, such as in `{{#example_in Examples/Intro.lean pointPosEvalNoType}}`, solves the problem:
+Adding an annotation, such as in `{{#example_in Examples/Intro.lean pointPosWithType}}`, solves the problem:
 ```Lean info
-{{#example_out Examples/Intro.lean pointPosEvalNoType}}
+{{#example_out Examples/Intro.lean pointPosWithType}}
 ```