Add the booleans concept

generators/Generator/Generator.lean

@@ -100,6 +100,7 @@ import Generator.AnagramGenerator
 import Generator.BobGenerator
 import Generator.MatchingBracketsGenerator
 import Generator.ReverseStringGenerator
+import Generator.GameNightGenerator
 
 import Std
 import Lean.Data.Json
@@ -112,6 +113,7 @@ abbrev endBodyGenerator := String -> String
 
 def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBodyGenerator) :=
   Std.HashMap.ofList [
+    ("GameNight", (GameNightGenerator.genIntro, GameNightGenerator.genTestCase, GameNightGenerator.genEnd)),
     ("MountainHike", (MountainHikeGenerator.genIntro, MountainHikeGenerator.genTestCase, MountainHikeGenerator.genEnd)),
     ("FruitStand", (FruitStandGenerator.genIntro, FruitStandGenerator.genTestCase, FruitStandGenerator.genEnd)),
     ("DotDsl", (DotDslGenerator.genIntro, DotDslGenerator.genTestCase, DotDslGenerator.genEnd)),

generators/Generator/Generator/GameNightGenerator.lean

@@ -0,0 +1,40 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace GameNightGenerator
+
+def genIntro (exercise : String) : String := s!"import LeanTest
+import {exercise}
+
+open LeanTest
+
+def {exercise.decapitalize}Tests : TestSuite :=
+  (TestSuite.empty \"{exercise}\")"
+
+def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
+  let input := case.get! "input"
+  let expected := case.get! "expected"
+  let description := case.get! "description"
+              |> (·.compress)
+  let funName := getFunName (case.get! "property")
+  let call := s!"({exercise}.{funName} {insertAllInputs input})"
+  let taskArg := match case.get? "task" with
+    | some task => s!" (taskId := some {task})"
+    | none => ""
+  s!"
+  |>.addTest {description} (do
+      return assertEqual {expected} {call}){taskArg}"
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end GameNightGenerator

reference/concepts/booleans/.meta/config.json

@@ -0,0 +1,6 @@
+{
+  "blurb": "Learn Lean's Bool type.",
+  "authors": [
+    "oxe-i"
+  ]
+}

reference/concepts/booleans/about.md

@@ -0,0 +1,64 @@
+# About
+
+`Bool` is the type of truth values.
+It has two values, `true` and `false`.
+
+```lean
+#eval true  -- true
+```
+
+## Combining Bool values
+
+`&&` is "and". 
+It is `true` only when both sides are `true`.
+
+```lean
+#eval true && false -- false
+#eval true && true  -- true
+```
+
+`||` is "or". 
+It is `true` when at least one side is `true`.
+
+```lean
+#eval true || false -- true
+#eval false || false -- false
+```
+
+`!` is "not". 
+It flips a `Bool`, so that `true` becomes `false` and `false` becomes `true`.
+
+```lean
+#eval !true  -- false
+#eval !false -- true
+```
+
+`^^` is "xor" (exclusive or). 
+It is `true` when exactly one side is `true`.
+If both sides are `false` or both are `true`, it is `false`.
+
+```lean
+#eval true ^^ false -- true
+#eval true ^^ true  -- false
+```
+
+## Short-circuit evaluation
+
+`&&` does not look at its right side when the left side is `false`.
+`||` does not look at its right side when the left side is `true`.
+This is called short-circuit evaluation.
+
+For example, `false && (some slow check)` skips the slow check entirely.
+The result is already known to be `false` from the left side alone.
+
+`^^` cannot short-circuit because its result always depends on both sides.
+
+## Comparing Bool values
+
+`Bool` supports `==` and `!=`, like `Nat` and `Int` do.
+
+```lean
+#eval true == true   -- true
+#eval true == false  -- false
+#eval true != false  -- true
+```

reference/concepts/booleans/introduction.md

@@ -0,0 +1,64 @@
+# Introduction
+
+`Bool` is the type of truth values.
+It has two values, `true` and `false`.
+
+```lean
+#eval true  -- true
+```
+
+## Combining Bool values
+
+`&&` is "and". 
+It is `true` only when both sides are `true`.
+
+```lean
+#eval true && false -- false
+#eval true && true  -- true
+```
+
+`||` is "or". 
+It is `true` when at least one side is `true`.
+
+```lean
+#eval true || false -- true
+#eval false || false -- false
+```
+
+`!` is "not". 
+It flips a `Bool`, so that `true` becomes `false` and `false` becomes `true`.
+
+```lean
+#eval !true  -- false
+#eval !false -- true
+```
+
+`^^` is "xor" (exclusive or). 
+It is `true` when exactly one side is `true`.
+If both sides are `false` or both are `true`, it is `false`.
+
+```lean
+#eval true ^^ false -- true
+#eval true ^^ true  -- false
+```
+
+## Short-circuit evaluation
+
+`&&` does not look at its right side when the left side is `false`.
+`||` does not look at its right side when the left side is `true`.
+This is called short-circuit evaluation.
+
+For example, `false && (some slow check)` skips the slow check entirely.
+The result is already known to be `false` from the left side alone.
+
+`^^` cannot short-circuit because its result always depends on both sides.
+
+## Comparing Bool values
+
+`Bool` supports `==` and `!=`, like `Nat` and `Int` do.
+
+```lean
+#eval true == true   -- true
+#eval true == false  -- false
+#eval true != false  -- true
+```

reference/concepts/booleans/links.json

@@ -0,0 +1,6 @@
+[
+  {
+    "url": "https://lean-lang.org/doc/reference/latest/Basic-Types/",
+    "description": "The Lean Language Reference: Basic Types, including Booleans"
+  }
+]

reference/config.json.additions

@@ -49,3 +49,27 @@
   ],
   "status": "beta"
 }
+
+// ---- booleans / game-night ----
+
+// Append to the top-level "concepts" array:
+{
+  "uuid": "5193a16c-2f38-48a6-8d23-c81fd5cd8a6e",
+  "slug": "booleans",
+  "name": "Booleans"
+}
+
+// Append to "exercises.concept":
+{
+  "slug": "game-night",
+  "name": "Game Night",
+  "uuid": "13718a3a-ad48-492a-951f-75e325c0537b",
+  "concepts": [
+    "booleans"
+  ],
+  "prerequisites": [
+    "basics",
+    "numbers"
+  ],
+  "status": "beta"
+}

reference/exercises/concept/fruit-stand/FruitStand.lean

@@ -1,6 +1,7 @@
 namespace FruitStand
 
-def applePrice : Nat := sorry --remove this line and define the constant
+def applePrice : Nat :=
+  sorry --remove this line and define the constant
 
 def revenue (applesSold : Nat) : Nat :=
   sorry --remove this line and implement the function

reference/exercises/concept/game-night/.docs/hints.md

@@ -0,0 +1,29 @@
+# Hints
+
+## General
+
+- [Basic Types][basic-types] in the Lean reference covers `Bool`, including `&&`, `||`, and `!`.
+- All five functions return a `Bool`, and need explicit parameter and return types, as usual.
+
+## 1. Check who can join
+
+- You can use [boolean operators][bool-operators] to combine the two parameters.
+
+## 2. Check who brings snacks
+
+- You can use [boolean operators][bool-operators] to combine the two parameters.
+
+## 3. Check who is skipping game night
+
+- You can use a [boolean operator][bool-operators] to invert the parameter.
+
+## 4. Check if two friends voted for the same game
+
+- Boolean values can be compared for equality.
+
+## 5. Check if there's exactly one scorekeeper
+
+- You can use [boolean operators][bool-operators] to combine the two parameters.
+
+[basic-types]: https://lean-lang.org/doc/reference/latest/Basic-Types/
+[bool-operators]: https://lean-lang.org/doc/reference/latest/Basic-Types/Booleans/#The-Lean-Language-Reference--Basic-Types--Booleans--Syntax

reference/exercises/concept/game-night/.docs/instructions.md

@@ -0,0 +1,54 @@
+# Instructions
+
+You are helping organize a game night with friends.
+
+## 1. Check who can join
+
+Define `canJoin`, a function with two `Bool` parameters, `hasConfirmed` and `isInvited`.
+The function returns `true` only when both are `true`.
+
+```lean
+#eval canJoin true true   -- true
+#eval canJoin true false  -- false
+```
+
+## 2. Check who brings snacks
+
+Define `bringsSnacks`, a function with two `Bool` parameters, `isHost` and `volunteered`.
+The function returns `true` when at least one of them is `true`.
+
+```lean
+#eval bringsSnacks true false  -- true
+#eval bringsSnacks false false -- false
+```
+
+## 3. Check who is skipping game night
+
+Define `isSkipping`, a function with one `Bool` parameter, `isComing`.
+It returns the opposite of `isComing`.
+
+```lean
+#eval isSkipping true  -- false
+#eval isSkipping false -- true
+```
+
+## 4. Check if two friends voted for the same game
+
+Define `votedSame`, a function with two `Bool` parameters, `firstVote` and `secondVote`.
+Each vote is `true` for "board game" and `false` for "video game".
+It returns `true` when both friends voted for the same kind of game.
+
+```lean
+#eval votedSame true true   -- true
+#eval votedSame true false  -- false
+```
+
+## 5. Check if there's exactly one scorekeeper
+
+Define `hasScorekeeper`, a function with two `Bool` parameters, `aVolunteers` and `bVolunteers`.
+It returns `true` only when exactly one of them is `true`.
+
+```lean
+#eval hasScorekeeper true false -- true
+#eval hasScorekeeper true true  -- false
+```

reference/exercises/concept/game-night/.docs/introduction.md

@@ -0,0 +1,64 @@
+# Introduction
+
+`Bool` is the type of truth values.
+It has two values, `true` and `false`.
+
+```lean
+#eval true  -- true
+```
+
+## Combining Bool values
+
+`&&` is "and". 
+It is `true` only when both sides are `true`.
+
+```lean
+#eval true && false -- false
+#eval true && true  -- true
+```
+
+`||` is "or". 
+It is `true` when at least one side is `true`.
+
+```lean
+#eval true || false -- true
+#eval false || false -- false
+```
+
+`!` is "not". 
+It flips a `Bool`, so that `true` becomes `false` and `false` becomes `true`.
+
+```lean
+#eval !true  -- false
+#eval !false -- true
+```
+
+`^^` is "xor" (exclusive or). 
+It is `true` when exactly one side is `true`.
+If both sides are `false` or both are `true`, it is `false`.
+
+```lean
+#eval true ^^ false -- true
+#eval true ^^ true  -- false
+```
+
+## Short-circuit evaluation
+
+`&&` does not look at its right side when the left side is `false`.
+`||` does not look at its right side when the left side is `true`.
+This is called short-circuit evaluation.
+
+For example, `false && (some slow check)` skips the slow check entirely.
+The result is already known to be `false` from the left side alone.
+
+`^^` cannot short-circuit because its result always depends on both sides.
+
+## Comparing Bool values
+
+`Bool` supports `==` and `!=`, like `Nat` and `Int` do.
+
+```lean
+#eval true == true   -- true
+#eval true == false  -- false
+#eval true != false  -- true
+```

reference/exercises/concept/game-night/.docs/introduction.md.tpl

@@ -0,0 +1 @@
+%{concept: booleans}