unify code for tactics and lemmas

client/src/components/Inventory.tsx

@@ -19,7 +19,7 @@ function Inventory({ tactics, lemmas } :
       <h2>Tactics</h2>
       <div className="inventory-list">
         { tactics.map(tac =>
-           <InventoryItem key={tac.name} showDoc={() => {setDocName(tac.name); setDocType("tactic")}}
+           <InventoryItem key={tac.name} showDoc={() => {setDocName(tac.name); setDocType("Tactic")}}
              name={tac.name} locked={tac.locked} disabled={tac.disabled} />) }
       {/* TODO: Click on Tactic: show info
         TODO: click on paste icon -> paste into command line */}
@@ -28,7 +28,7 @@ function Inventory({ tactics, lemmas } :
       <h2>Lemmas</h2>
       <div className="inventory-list">
         { lemmas.map(lem =>
-            <InventoryItem key={lem.name} showDoc={() => {setDocName(lem.name); setDocType("lemma")}}
+            <InventoryItem key={lem.name} showDoc={() => {setDocName(lem.name); setDocType("Lemma")}}
               name={lem.name} locked={lem.locked} disabled={lem.disabled} />) }
       </div>
 

server/leanserver/GameServer/Commands.lean

@@ -180,92 +180,119 @@ macro "Hint" decls:mydecl* ":" goal:term "=>" msg:str : command => do
 macro "HiddenHint" decls:mydecl* ":" goal:term "=>" msg:str : command => do
   `(set_option linter.unusedVariables false in HiddenHint' $decls* : $goal => $msg)
 
-/-! ## Tactics -/
+/-! ## Inventory -/
+
+/-- Throw an error if inventory doc does not exist -/
+def checkInventoryDoc (type : InventoryType) (name : Name) : CommandElabM Unit := do
+  let some _ := (inventoryDocExt.getState (← getEnv)).find?
+      (fun x => x.name == name && x.type == type)
+    | throwError "Missing {type} Documentation: {name}"
+
+/-! ### Tactics -/
 
 /-- Declare a documentation entry for some tactic.
 Expect an identifier and then a string literal. -/
 elab "TacticDoc" name:ident content:str : command =>
-  modifyEnv (tacticDocExt.addEntry · {
+  modifyEnv (inventoryDocExt.addEntry · {
+    category := default
+    type := .Tactic
     name := name.getId,
+    userName := name.getId,
     content := content.getString })
 
-instance : Quote TacticDocEntry `term :=
-⟨λ entry => Syntax.mkCApp ``TacticDocEntry.mk #[quote entry.name, quote entry.content]⟩
-
-/-- Throw an error if tactic doc does not exist -/
-def checkTacticDoc (name : Name) : CommandElabM Unit := do
-  let some _ := (tacticDocExt.getState (← getEnv)).find? (·.name = name)
-    | throwError "Missing Tactic Documentation: {name}"
-
 /-- Declare tactics that are introduced by this level. -/
 elab "NewTactics" args:ident* : command => do
   let names := args.map (·.getId)
-  for name in names do checkTacticDoc name
-  modifyCurLevel fun level => pure {level with newTactics := names}
+  for name in names do checkInventoryDoc .Tactic name
+  modifyCurLevel fun level => pure {level with tactics := {level.tactics with new := names}}
 
 /-- Declare tactics that are temporarily disabled in this level -/
 elab "DisabledTactics" args:ident* : command => do
   let names := args.map (·.getId)
-  for name in names do checkTacticDoc name
-  modifyCurLevel fun level => pure {level with disabledTactics := names}
+  for name in names do checkInventoryDoc .Tactic name
+  modifyCurLevel fun level => pure {level with tactics := {level.tactics with disabled := names}}
 
 /-- Temporarily disable all tactics except the ones declared here -/
 elab "OnlyTactics" args:ident* : command => do
   let names := args.map (·.getId)
-  for name in names do checkTacticDoc name
-  modifyCurLevel fun level => pure {level with onlyTactics := names}
+  for name in names do checkInventoryDoc .Tactic name
+  modifyCurLevel fun level => pure {level with tactics := {level.tactics with only := names}}
 
-/-! ## Lemmas -/
+/-! ### Definitions -/
+
+/-- Declare a documentation entry for some definition.
+Expect an identifier and then a string literal. -/
+elab "DefinitionDoc" name:ident content:str : command =>
+  modifyEnv (inventoryDocExt.addEntry · {
+    category := default
+    type := .Definition
+    name := name.getId,
+    userName := name.getId,
+    content := content.getString })
+
+/-- Declare definitions that are introduced by this level. -/
+elab "NewDefinitions" args:ident* : command => do
+  let names := args.map (·.getId)
+  for name in names do checkInventoryDoc .Definition name
+  modifyCurLevel fun level => pure {level with definitions := {level.definitions with new := names}}
+
+/-- Declare definitions that are temporarily disabled in this level -/
+elab "DisabledDefinitions" args:ident* : command => do
+  let names := args.map (·.getId)
+  for name in names do checkInventoryDoc .Definition name
+  modifyCurLevel fun level => pure {level with definitions := {level.definitions with disabled := names}}
+
+/-- Temporarily disable all definitions except the ones declared here -/
+elab "OnlyDefinitions" args:ident* : command => do
+  let names := args.map (·.getId)
+  for name in names do checkInventoryDoc .Definition name
+  modifyCurLevel fun level => pure {level with definitions := {level.definitions with only := names}}
+
+
+/-! ### Lemmas -/
 
 /-- Declare a documentation entry for some lemma.
 Expect two identifiers and then a string literal. The first identifier is meant
 as the real name of the lemma while the second is the displayed name. Currently
 the real name isn't used. -/
 elab "LemmaDoc" name:ident "as" userName:ident "in" category:str content:str : command =>
-  modifyEnv (lemmaDocExt.addEntry · {
+  modifyEnv (inventoryDocExt.addEntry · {
     name := name.getId,
+    type := .Lemma
     userName := userName.getId,
     category := category.getString,
     content := content.getString })
 
-/-- Declare a set of lemma documentation entries.
-Expect an identifier used as the set name then `:=` and a
-space separated list of identifiers. -/
-elab "LemmaSet" name:ident ":" title:str ":=" args:ident* : command => do
-  let docs := lemmaDocExt.getState (← getEnv)
-  let mut entries : Array Name := #[]
-  for arg in args do
-    let name := arg.getId
-    match docs.find? (·.userName = name) with
-    | some doc => entries := entries.push name
-    | none => throwError "Lemma doc {name} wasn't found."
-  modifyEnv (lemmaSetExt.addEntry · {
-    name := name.getId,
-    title := title.getString,
-    lemmas := entries })
+/-- Declare lemmas that are introduced by this level. -/
+elab "NewLemmas" args:ident* : command => do
+  let names := args.map (·.getId)
+  for name in names do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with new := names}}
 
-instance : Quote LemmaDocEntry `term :=
-⟨λ entry => Syntax.mkCApp ``LemmaDocEntry.mk #[quote entry.name, quote entry.userName, quote entry.category, quote entry.content]⟩
+/-- Declare lemmas that are temporarily disabled in this level -/
+elab "DisabledLemmas" args:ident* : command => do
+  let names := args.map (·.getId)
+  for name in names do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with disabled := names}}
 
-/-- Declare the list of lemmas that will be displayed in the current level.
-Expects a space separated list of identifiers that refer to either a lemma doc
-entry or a lemma doc set. -/
-elab "NewLemmas" args:ident* : command => do
-  let env ← getEnv
-  let docs := lemmaDocExt.getState env
-  let sets := lemmaSetExt.getState env
-  let mut lemmas : Array Name := #[]
-  for arg in args do
-    let name := arg.getId
-    match docs.find? (·.userName = name) with
-    | some entry => lemmas := lemmas.push name
-    | none => match sets.find? (·.name = name) with
-              | some entry => lemmas := lemmas ++ entry.lemmas
-              | none => throwError "Lemma doc or lemma set {name} wasn't found."
-  modifyCurLevel fun level => pure {level with newLemmas := lemmas}
+/-- Temporarily disable all lemmas except the ones declared here -/
+elab "OnlyLemmas" args:ident* : command => do
+  let names := args.map (·.getId)
+  for name in names do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with only := names}}
 
 /-! ## Make Game -/
 
+def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
+| .Tactic => level.tactics
+| .Definition => level.definitions
+| .Lemma => level.lemmas
+
+def GameLevel.setComputedInventory (level : GameLevel) : InventoryType → Array Availability → GameLevel
+| .Tactic, v =>     {level with tactics     := {level.tactics     with computed := v}}
+| .Definition, v => {level with definitions := {level.definitions with computed := v}}
+| .Lemma, v =>      {level with lemmas      := {level.lemmas      with computed := v}}
+
 /-- Make the final Game. This command will precompute various things about the game, such as which
 tactics are available in each level etc. -/
 elab "MakeGame" : command => do
@@ -275,72 +302,47 @@ elab "MakeGame" : command => do
   if game.worlds.hasLoops then
     throwError "World graph has loops!"
 
-  -- Compute which tactics/lemmas are available in which level:
-  let mut newTacticsInWorld : HashMap Name (HashSet Name) := {}
-  let mut allTactics : HashSet Name := {}
-  let mut newLemmasInWorld : HashMap Name (HashSet Name) := {}
-  let mut allLemmas : HashSet Name := {}
-  for (worldId, world) in game.worlds.nodes.toArray do
-    let mut newTactics : HashSet Name:= {}
-    let mut newLemmas : HashSet Name:= {}
-    for (_, level) in world.levels.toArray do
-      newTactics := newTactics.insertMany level.newTactics
-      allTactics := allTactics.insertMany level.newTactics
-      newLemmas := newLemmas.insertMany level.newLemmas
-      allLemmas := allLemmas.insertMany level.newLemmas
-    newTacticsInWorld := newTacticsInWorld.insert worldId newTactics
-    newLemmasInWorld := newLemmasInWorld.insert worldId newLemmas
-
-  -- Basic tactic/lemma availability: all locked, none disabled.
-  let Availability₀ : HashMap Name Availability :=
-    HashMap.ofList $
-      allTactics.toList.map fun name =>
-        (name, {name, locked := true, disabled := false})
-  let lemmaAvailability₀ : HashMap Name Availability :=
-    HashMap.ofList $
-      allLemmas.toList.map fun name =>
-        (name, {name, locked := true, disabled := false})
-
-  -- Availability after a given world
-  let mut tacticsInWorld : HashMap Name (HashMap Name Availability) := {}
-  let mut lemmasInWorld : HashMap Name (HashMap Name Availability) := {}
-  for (worldId, _) in game.worlds.nodes.toArray do
-    let mut tactics := Availability₀
-    let mut lemmas := lemmaAvailability₀
-    let predecessors := game.worlds.predecessors worldId
-    for predWorldId in predecessors do
-      for tac in newTacticsInWorld.find! predWorldId do
-        tactics := tactics.insert tac {name := tac, locked := false, disabled := false}
-      for lem in newLemmasInWorld.find! predWorldId do
-        lemmas := lemmas.insert lem {name := lem, locked := false, disabled := false}
-    tacticsInWorld := tacticsInWorld.insert worldId tactics
-    lemmasInWorld := lemmasInWorld.insert worldId lemmas
-
-  for (worldId, world) in game.worlds.nodes.toArray do
-    let mut tactics := tacticsInWorld.find! worldId
-    let mut lemmas := lemmasInWorld.find! worldId
-
-    let levels := world.levels.toArray.insertionSort fun a b => a.1 < b.1
-
-    for (levelId, level) in levels do
-      for tac in level.newTactics do
-        tactics := tactics.insert tac {name := tac, locked := false, disabled := false}
-      for tac in level.disabledTactics do
-        tactics := tactics.insert tac {name := tac, locked := false, disabled := true}
-      for lem in level.newLemmas do
-        lemmas := lemmas.insert lem {name := lem, locked := false, disabled := false}
-      for lem in level.disabledLemmas do
-        lemmas := lemmas.insert lem {name := lem, locked := false, disabled := true}
-
-      let tacticArray := tactics.toArray
-        |>.insertionSort (fun a b => a.1.toString < b.1.toString)
-        |>.map (·.2)
-
-      let lemmaArray := lemmas.toArray
-        |>.insertionSort (fun a b => a.1.toString < b.1.toString)
-        |>.map (·.2)
-
-      modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
-        return {level with
-          tactics := tacticArray
-          lemmas := lemmaArray}
+  -- Compute which inventory items are available in which level:
+  for inventoryType in open InventoryType in #[Tactic, Definition, Lemma] do
+    let mut newItemsInWorld : HashMap Name (HashSet Name) := {}
+    let mut allItems : HashSet Name := {}
+    for (worldId, world) in game.worlds.nodes.toArray do
+      let mut newItems : HashSet Name := {}
+      for (_, level) in world.levels.toArray do
+        newItems := newItems.insertMany (level.getInventory inventoryType).new
+        allItems := allItems.insertMany (level.getInventory inventoryType).new
+      newItemsInWorld := newItemsInWorld.insert worldId newItems
+
+    -- Basic inventory item availability: all locked, none disabled.
+    let Availability₀ : HashMap Name Availability :=
+      HashMap.ofList $
+        allItems.toList.map fun name =>
+          (name, {name, locked := true, disabled := false})
+
+    -- Availability after a given world
+    let mut itemsInWorld : HashMap Name (HashMap Name Availability) := {}
+    for (worldId, _) in game.worlds.nodes.toArray do
+      let mut items := Availability₀
+      let predecessors := game.worlds.predecessors worldId
+      for predWorldId in predecessors do
+        for item in newItemsInWorld.find! predWorldId do
+          items := items.insert item {name := item, locked := false, disabled := false}
+      itemsInWorld := itemsInWorld.insert worldId items
+
+    for (worldId, world) in game.worlds.nodes.toArray do
+      let mut items := itemsInWorld.find! worldId
+
+      let levels := world.levels.toArray.insertionSort fun a b => a.1 < b.1
+
+      for (levelId, level) in levels do
+        for item in (level.getInventory inventoryType).new do
+          items := items.insert item {name := item, locked := false, disabled := false}
+        for item in (level.getInventory inventoryType).disabled do
+          items := items.insert item {name := item, locked := false, disabled := true}
+
+        let itemsArray := items.toArray
+          |>.insertionSort (fun a b => a.1.toString < b.1.toString)
+          |>.map (·.2)
+
+        modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
+          return level.setComputedInventory inventoryType itemsArray

server/leanserver/GameServer/EnvExtensions.lean

@@ -26,77 +26,43 @@ structure GoalHintEntry where
   hidden : Bool := false
   deriving Repr
 
-/-! ## Tactic documentation -/
 
-structure TacticDocEntry where
-  name : Name
-  content : String
-  deriving ToJson, Repr
+/-! ## Tactic/Definition/Lemma documentation -/
 
-/-- Environment extension for tactic documentation. -/
-initialize tacticDocExt : SimplePersistentEnvExtension TacticDocEntry (Array TacticDocEntry) ←
-  registerSimplePersistentEnvExtension {
-    name := `tactic_doc
-    addEntryFn := Array.push
-    addImportedFn := Array.concatMap id
-  }
+inductive InventoryType := | Tactic | Lemma | Definition
+deriving ToJson, FromJson, Repr, BEq, Hashable
 
-def getTacticDoc? {m : Type → Type} [Monad m] [MonadEnv m] (tac : Name) :
-    m (Option TacticDocEntry) := do
-  return (tacticDocExt.getState (← getEnv)).find? (·.name = tac)
-
-open Elab Command in
-/-- Print a registered tactic doc for debugging purposes. -/
-elab "#print_tactic_doc" : command => do
-  for entry in tacticDocExt.getState (← getEnv) do
-    dbg_trace "{entry.name} : {entry.content}"
-
-/-! ## Lemma documentation -/
+instance : ToString InventoryType := ⟨fun t => match t with
+| .Tactic => "Tactic"
+| .Lemma => "Lemma"
+| .Definition => "Definition"
+⟩
 
-structure LemmaDocEntry where
+structure InventoryDocEntry where
   name : Name
+  type : InventoryType
   userName : Name
   category : String
   content : String
   deriving ToJson, Repr
 
-/-- Environment extension for lemma documentation. -/
-initialize lemmaDocExt : SimplePersistentEnvExtension LemmaDocEntry (Array LemmaDocEntry) ←
+/-- Environment extension for inventory documentation. -/
+initialize inventoryDocExt : SimplePersistentEnvExtension InventoryDocEntry (Array InventoryDocEntry) ←
   registerSimplePersistentEnvExtension {
-    name := `lemma_doc
+    name := `inventory_doc
     addEntryFn := Array.push
     addImportedFn := Array.concatMap id
   }
 
-def getLemmaDoc? {m : Type → Type} [Monad m] [MonadEnv m] (tac : Name) :
-    m (Option LemmaDocEntry) := do
-  return (lemmaDocExt.getState (← getEnv)).find? (·.name = tac)
+def getInventoryDoc? {m : Type → Type} [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
+    m (Option InventoryDocEntry) := do
+  return (inventoryDocExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
 
 open Elab Command in
-/-- Print a lemma doc for debugging purposes. -/
-elab "#print_lemma_doc" : command => do
-  for entry in lemmaDocExt.getState (← getEnv) do
-    dbg_trace "{entry.userName} ({entry.name}) in {entry.category}: {entry.content}"
-
-structure LemmaSetEntry where
-  name : Name
-  title : String
-  lemmas : Array Name
-  deriving ToJson, Repr
-
-/-- Environment extension for lemma sets. -/
-initialize lemmaSetExt : SimplePersistentEnvExtension LemmaSetEntry (Array LemmaSetEntry) ←
-  registerSimplePersistentEnvExtension {
-    name := `lemma_set
-    addEntryFn := Array.push
-    addImportedFn := Array.concatMap id
-  }
-
-open Elab Command in
-/-- Print all registered lemma sets for debugging purposes. -/
-elab "#print_lemma_set" : command => do
-  for entry in lemmaSetExt.getState (← getEnv) do
-    dbg_trace "{entry.name} : {entry.lemmas}"
+/-- Print a registered tactic doc for debugging purposes. -/
+elab "#print_doc" : command => do
+  for entry in inventoryDocExt.getState (← getEnv) do
+    dbg_trace "[{entry.type}] {entry.name} : {entry.content}"
 
 
 /-! ## Environment extensions for game specification-/
@@ -156,7 +122,18 @@ structure Availability where
   name : Name
   locked : Bool
   disabled : Bool
-deriving ToJson, FromJson, Repr
+deriving ToJson, FromJson, Repr, Inhabited
+
+structure InventoryInfo where
+  -- new inventory items introduced by this level:
+  new : Array Name
+  -- inventory items exceptionally forbidden in this level:
+  disabled : Array Name
+  -- only these inventory items are allowed in this level (ignored if empty):
+  only : Array Name
+  -- inventory items in this level (computed by `MakeGame`):
+  computed : Array Availability
+deriving ToJson, FromJson, Repr, Inhabited
 
 def getCurLevelId [MonadError m] : m LevelId := do
   return { game := ← getCurGameId, world := ← getCurWorldId, level := ← getCurLevelIdx}
@@ -164,37 +141,20 @@ def getCurLevelId [MonadError m] : m LevelId := do
 /-- Instance to make GameLevel Repr work -/
 instance : Repr Elab.Command.Scope := ⟨fun s _ => repr s.currNamespace⟩
 
-/--
-Fields:
-- TODO
-- introduction: Theory block shown all the time.
-- description:  The mathematical statemtent in mathematician-readable form.
-- goal:         The statement in Lean.
-- conclusion:   Displayed when level is completed.
--/
 structure GameLevel where
   index: Nat
   title: String := default
+  /-- introduction: Theory block shown all the time -/
   introduction: String := default
+  /-- The mathematical statemtent in mathematician-readable form -/
   description: String := default
+  /-- conclusion displayed when level is completed. -/
   conclusion: String := default
-  -- new tactics introduces by this level:
-  newTactics: Array Name := default
-  -- tactics exceptionally forbidden in this level:
-  disabledTactics: Array Name := default
-  -- only these tactics are allowed in this level (ignore if empty):
-  onlyTactics: Array Name := default
-  -- tactics in this level (computed by `MakeGame`):
-  tactics: Array Availability := default
-  -- new lemmas introduces by this level:
-  newLemmas: Array Name := default
-  -- lemmas exceptionally forbidden in this level:
-  disabledLemmas: Array Name := default
-  -- only these lemmas are allowed in this level (ignore if empty):
-  onlyLemmas: Array Name := default
-  -- lemmas in this level (computed by `MakeGame`):
-  lemmas: Array Availability := default
+  tactics: InventoryInfo := default
+  definitions: InventoryInfo := default
+  lemmas: InventoryInfo := default
   hints: Array GoalHintEntry := default
+  /-- The statement in Lean. -/
   goal : TSyntax `Lean.Parser.Command.declSig := default
   scope : Elab.Command.Scope := default
   descrText: String := default

server/leanserver/GameServer/Game.lean

@@ -66,27 +66,11 @@ structure Doc where
   text: String
 deriving ToJson
 
-inductive TacOrLem := | tactic | «lemma»
-deriving ToJson, FromJson
-
 structure LoadDocParams where
   name : Name
-  type : TacOrLem
+  type : InventoryType
 deriving ToJson, FromJson
 
-def mkDoc (name : Name) (type : TacOrLem) : GameServerM (Option Doc) := do
-  match type with
-  | .tactic => do
-    let doc ← getTacticDoc? name
-    return doc.map fun doc =>
-      { name := doc.name.toString
-        text := doc.content }
-  | .lemma => do
-    let doc ← getLemmaDoc? name
-    return doc.map fun doc =>
-      { name := doc.name.toString
-        text := doc.content }
-
 def handleDidOpenLevel (params : Json) : GameServerM Unit := do
   let p ← parseParams _ params
   let m := p.textDocument
@@ -105,8 +89,8 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
     param  := {
       uri       := m.uri
       levelModule := lvl.module
-      tactics := lvl.tactics
-      lemmas := lvl.lemmas
+      tactics := lvl.tactics.computed
+      lemmas := lvl.lemmas.computed
       : DidOpenLevelParams
     }
   }
@@ -133,8 +117,8 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
       let levelInfo : LevelInfo :=
           { index := lvl.index,
             title := lvl.title,
-            tactics := lvl.tactics,
-            lemmas := lvl.lemmas,
+            tactics := lvl.tactics.computed,
+            lemmas := lvl.lemmas.computed,
             descrText := lvl.descrText,
             descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
             introduction := lvl.introduction }
@@ -144,10 +128,13 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
       let p ← parseParams LoadDocParams (toJson params)
       let s ← get
       let c ← read
-      let some doc ← mkDoc p.name p.type
+      let some doc ← getInventoryDoc? p.name p.type
         | do
             c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Documentation not found: {p.name}", none⟩
             return true
+      let doc : Doc :=
+          { name := doc.name.toString
+            text := doc.content }
       c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩
       return true
     | _ => return false

server/testgame/TestGame/LemmaDocs.lean

@@ -55,9 +55,6 @@ LemmaDoc add_zero as add_zero in "Addition"
 LemmaDoc add_succ as add_succ in "Addition"
 "This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`."
 
-LemmaSet addition : "Addition lemmas" :=
-zero_add add_zero
-
 LemmaDoc not_forall as not_forall in "Logic"
 "`∀ (A : Prop), ¬(∀ x, A) ↔ ∃x, (¬A)`."
 
@@ -106,14 +103,6 @@ LemmaDoc Nat.prime_def_lt'' as Nat.prime_def_lt'' in "Nat"
 ""
 
 
-
-
-LemmaSet natural : "Natürliche Zahlen" :=
-Even Odd not_odd not_even
-
-LemmaSet logic : "Logik" :=
-not_not not_forall not_exists
-
 LemmaDoc Finset.sum_add_distrib as Finset.sum_add_distrib in "Sum"
 ""