diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index a230f45..6316e89 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -413,63 +413,67 @@ export function CommandLineInterface(props: { world: string, level: number, data
- {proof.length ? proof.map((step, i) => {
- if (i == proof.length - 1 && hasInteractiveErrors(step.errors)) {
- // if the last command contains an error, we only display the errors but not the
- // entered command as it is still present in the command line.
- // TODO: Should not use index as key.
- return
- {props.data?.introduction}
+ {proof.length ?
+ <>
+ {proof.map((step, i) => {
+ if (i == proof.length - 1 && hasInteractiveErrors(step.errors)) {
+ // if the last command contains an error, we only display the errors but not the
+ // entered command as it is still present in the command line.
+ // TODO: Should not use index as key.
+ return
+
- }
- {mobile && <>
-
- {i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
-
- }
- >
- }
-
- {/* Show a message that there are no goals left */}
- {!step.goals.length && (
-
- {completed ?
-
Level completed! 🎉
:
-
- no goals left
- This probably means you solved the level with warnings or Lean encountered a parsing error.
-