From 0a2d14e01f0a994059cebf5199156d9c6f17da93 Mon Sep 17 00:00:00 2001 From: Thomas Sibut-Pinote Date: Tue, 7 Jun 2016 10:06:27 +0100 Subject: [PATCH] typo: exmaple --> example --- 05_Interacting_with_Lean.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/05_Interacting_with_Lean.org b/05_Interacting_with_Lean.org index 4088fcb8..59c88a4d 100644 --- a/05_Interacting_with_Lean.org +++ b/05_Interacting_with_Lean.org @@ -180,7 +180,7 @@ you wish to use. The command =import standard= imports the essential parts of the standard library, and by now you have seen many of the namespaces you -will need. For exmaple, you should =open nat= for notation when you +will need. For example, you should =open nat= for notation when you are working with the natural numbers, and =open int= when you are working with the integers. In general, however, it is important for you to be familiar with the library and its contents, so you know what