From 98a6ebdaddae50f5a4e2d46d4e2937cb5c0f9d37 Mon Sep 17 00:00:00 2001 From: Elliot Date: Tue, 4 Jul 2023 17:33:45 -0400 Subject: [PATCH] Fix missing word in intro.lean I have just started playing the the natural number game at https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/. I was reading the intro and noticed a word missing in the following sentence: `In this game, you get own version of the natural numbers, called mynat, in an interactive theorem prover called Lean.` It seems that there is a missing word before `own`. Should it be `In this game, you get your own version [..]`? Thank you for reviewing my proposed fix. --- src/game/intro.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/game/intro.lean b/src/game/intro.lean index 0df3862..9fbf292 100644 --- a/src/game/intro.lean +++ b/src/game/intro.lean @@ -10,7 +10,7 @@ Blue nodes on the graph are ones that you are ready to enter. Grey nodes you sho from -- a grey node turns blue when *all* nodes above it are complete. Green nodes are completed. (Actually you can try any level at any time, but you might not know enough to complete it if it's grey). -In this game, you get own version of the natural numbers, called `mynat`, in an interactive +In this game, you get your own version of the natural numbers, called `mynat`, in an interactive theorem prover called Lean. Your version of the natural numbers satisfies something called the principle of mathematical induction, and a couple of other things too (Peano's axioms). Unfortunately, nobody has proved any theorems about these