diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 9cdfc67..1b03b0a 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -313,7 +313,7 @@ partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : Co return {acc with definitions := acc.definitions.insertMany ns} ) acc -#check expandOptDocComment? +-- #check expandOptDocComment? /-- Define the statement of the current level. -/ elab doc:docComment ? attrs:Parser.Term.attributes ? diff --git a/server/lean-toolchain b/server/lean-toolchain index 9b1d5d7..f0a6d66 100644 --- a/server/lean-toolchain +++ b/server/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.0.0-rc4 +leanprover/lean4:v4.0.0