minor

anoma · Dec 17, 2024 · 5f7b5db · 5f7b5db
1 parent 218a3df
commit 5f7b5db
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git a/Juvix/Core/Main/Semantics.lean b/Juvix/Core/Main/Semantics.lean
@@ -1,7 +1,6 @@
 
 import Juvix.Core.Main.Language
 import Mathlib.Tactic.CC
-import Aesop
 
 namespace Juvix.Core.Main
 
@@ -115,7 +114,7 @@ inductive Value.Terminating (P : Program) : Value → Prop where
     Value.Terminating P (Value.constr_app ctr_name args_rev)
   | closure {ctx body} :
     (∀ v v',
-      [P] (v :: ctx) ⊢ body ↦ v' →
+      [P] v :: ctx ⊢ body ↦ v' →
       Value.Terminating P v') →
     Value.Terminating P (Value.closure ctx body)
   | unit : Value.Terminating P Value.unit

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "07b2399c02d91a83fc030d165d734dca8d92a806",
+   "rev": "bb0575e329e059f7ec31c43337a2094282f6be3c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "74dffd1a83cdd2969a31c9892b0517e7c6f50668",
+   "rev": "9e583efcea920afa13ee2a53069821a2297a94c0",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",