From 0a6ebbe86241dfff777d5204a96ec5e7ba0f9b61 Mon Sep 17 00:00:00 2001 From: David Christiansen Date: Sun, 17 Jul 2022 09:59:22 +0200 Subject: [PATCH] Fix copy-paste mistake Fixes #37 --- .../src/getting-to-know/conveniences.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/functional-programming-lean/src/getting-to-know/conveniences.md b/functional-programming-lean/src/getting-to-know/conveniences.md index cf8f85e..40667f4 100644 --- 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}} ```