Update to Lean toolchain 4.22.0.

Author: abdoo8080

PreBuild.lean

@@ -527,8 +527,8 @@ def writeLean (cpp lean :  FilePath) : IO Unit := do
 namespace FilePath
 
 def modified (p : FilePath) : IO Time := do
-  let meta ← p.metadata
-  return meta.modified
+  let metadata ← p.metadata
+  return metadata.modified
 
 end FilePath
 

cvc5Test/Unit/ApiKind.lean

@@ -18,8 +18,8 @@ test![TestApiKind, kindHash] _tm => do
   for idx in [Kind.INTERNAL_KIND.toCtorIdx : Kind.LAST_KIND.toCtorIdx] do
     let k := Kind.ofNat idx
     if k = Kind.INTERNAL_KIND then
-      assertEq (k.hash + 2) UInt64.size
+      assertEq (k.hash + 2) ⟨UInt64.size⟩
     else if k  = Kind.UNDEFINED_KIND then
-      assertEq (k.hash + 1) UInt64.size
+      assertEq (k.hash + 1) ⟨UInt64.size⟩
     else
-      assertEq (k.hash + 2) k.toCtorIdx
+      assertEq (k.hash + 2) ⟨k.toCtorIdx⟩

cvc5Test/Unit/ApiProofRule.lean

@@ -16,7 +16,7 @@ test![TestApiBlackProofRule, proofRuleToString] _tm => do
 test![TestApiBlackProofRule, proofRuleHash] _tm => do
   for idx in [ProofRule.ASSUME.toCtorIdx : ProofRule.UNKNOWN.toCtorIdx] do
     let pr := ProofRule.ofNat idx
-    assertEq pr.hash pr.toCtorIdx
+    assertEq pr.hash ⟨pr.toCtorIdx⟩
 
 test![TestApiBlackProofRewriteRule, proofRuleToString] _tm => do
   for idx in [ProofRule.ASSUME.toCtorIdx : ProofRule.UNKNOWN.toCtorIdx] do
@@ -27,4 +27,4 @@ test![TestApiBlackProofRewriteRule, proofRuleToString] _tm => do
 test![TestApiBlackProofRewriteRule, proofRuleHash] _tm => do
   for idx in [ProofRule.ASSUME.toCtorIdx : ProofRule.UNKNOWN.toCtorIdx] do
     let pr := ProofRule.ofNat idx
-    assertEq pr.hash pr.toCtorIdx
+    assertEq pr.hash ⟨pr.toCtorIdx⟩

cvc5Test/Unit/ApiSkolemId.lean

@@ -16,5 +16,5 @@ test![TestApiBlackSkolemId, skolemIdToString] _tm => do
 test![TestApiBlackSkolemId, skolemIdHash] _tm => do
   for idx in [SkolemId.INTERNAL.toCtorIdx : SkolemId.NONE.toCtorIdx] do
     let si := SkolemId.ofNat idx
-    assertEq si.hash si.toCtorIdx
+    assertEq si.hash ⟨si.toCtorIdx⟩
   assertNe SkolemId.PURIFY.hash SkolemId.INTERNAL.hash

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.21.0
+leanprover/lean4:v4.22.0