Update Tue May 28 16:36:12 BST 2024

hrmacbeth · May 28, 2024 · 7c502ea · 7c502ea
1 parent e0f41e8
commit 7c502ea
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/.gitignore b/.gitignore
@@ -1,4 +1,3 @@
-/.vscode
 *.olean
 /_target
 /.lake/

diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -0,0 +1,8 @@
+{
+    "editor.semanticHighlighting.enabled": true,
+    "editor.minimap.enabled": false,
+    "editor.rulers": [100],
+    "lean4.infoview.showExpectedType": false,
+    "lean4.infoview.emphasizeFirstGoal": true,
+    "lean4.infoview.showGoalNames": false,
+}