From 96a8da9d9317884918eb7213684c5ba5616369b1 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 31 Mar 2023 12:10:09 +0200 Subject: [PATCH] Apply suggestions from code review --- server/adam/Adam.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/adam/Adam.lean b/server/adam/Adam.lean index 884e426..1402b0c 100644 --- a/server/adam/Adam.lean +++ b/server/adam/Adam.lean @@ -27,7 +27,7 @@ Introduction Willkommen zu unserem Prototyp eines Lean4-Lernspiels. Hier lernst du computer-gestützte Beweisführung. Das Interface ist etwas vereinfacht, aber wenn du den *Editor Mode* aktivierst, fühlt es sich -fast genauso an wie eine professionalle IDE, etwa VSCode. +fast genauso an wie in VSCode, der standard IDE für Lean. Rechts siehst du eine Übersicht. Das Spiel besteht aus mehreren Planeten, und jeder Planet hat mehrere Levels, die in Form von grauen Punkten dargestellt sind. Gelöste Levels werden grün.