refactor: avoid using LocalDecl constructors directly

This PR makes changes for compatibility with leanprover/lean4#8804.

The key difference is that `nondep := true` should be treated as a cdecl. The `LocalDecl.isLet` will return false for such ldecls.

Author: kmill

Aesop/RuleTac/GoalDiff.lean

@@ -65,13 +65,13 @@ protected def GoalDiff.empty (oldGoal newGoal : MVarId) : GoalDiff := {
 def isRPINFEqual (goal₁ goal₂ : MVarId) (e₁ e₂ : Expr) : BaseM Bool :=
   return (← goal₁.withContext $ rpinf e₁) == (← goal₂.withContext $ rpinf e₂)
 
-def isRPINFEqualLDecl (goal₁ goal₂ : MVarId) :
-    (ldecl₁ ldecl₂ : LocalDecl) → BaseM Bool
-  | .cdecl (type := type₁) .., .cdecl (type := type₂) .. =>
-    isRPINFEqual goal₁ goal₂ type₁ type₂
-  | .ldecl (type := type₁) (value := value₁) .., .ldecl (type := type₂) (value := value₂) .. =>
-    isRPINFEqual goal₁ goal₂ type₁ type₂ <&&>
-    isRPINFEqual goal₁ goal₂ value₁ value₂
+def isRPINFEqualLDecl (goal₁ goal₂ : MVarId) (ldecl₁ ldecl₂ : LocalDecl) : BaseM Bool :=
+  match ldecl₁.isLet, ldecl₂.isLet with
+  | false, false =>
+    isRPINFEqual goal₁ goal₂ ldecl₁.type ldecl₂.type
+  | true, true =>
+    isRPINFEqual goal₁ goal₂ ldecl₁.type ldecl₂.type <&&>
+    isRPINFEqual goal₁ goal₂ ldecl₁.value ldecl₂.value
   | _, _ => return false
 
 def getNewFVars (oldGoal newGoal : MVarId) (oldLCtx newLCtx : LocalContext) :

Aesop/Util/EqualUpToIds.lean

@@ -281,19 +281,18 @@ mutual
       | _, _ => return false
 
   @[specialize]
-  unsafe def localDeclsEqualUpToIdsCore :
-      LocalDecl → LocalDecl → ReaderT GoalContext EqualUpToIdsM Bool
-    | .cdecl _ _ userName₁ type₁ bi₁ kind₁,
-      .cdecl _ _ userName₂ type₂ bi₂ kind₂ =>
-      pure (namesEqualUpToMacroScopes userName₁ userName₂ && bi₁ == bi₂ &&
-            kind₁ == kind₂) <&&>
-      exprsEqualUpToIdsCore₁ type₁ type₂
-    | .ldecl _ _ userName₁ type₁ v₁ _ kind₁,
-      .ldecl _ _ userName₂ type₂ v₂ _ kind₂ =>
-      pure (namesEqualUpToMacroScopes userName₁ userName₂ &&
-            kind₁ == kind₂) <&&>
-      exprsEqualUpToIdsCore₁ type₁ type₂ <&&>
-      exprsEqualUpToIdsCore₁ v₁ v₂
+  unsafe def localDeclsEqualUpToIdsCore (ldecl₁ ldecl₂ : LocalDecl) :
+      ReaderT GoalContext EqualUpToIdsM Bool :=
+    match ldecl₁.isLet, ldecl₂.isLet with
+    | false, false =>
+      pure (namesEqualUpToMacroScopes ldecl₁.userName ldecl₂.userName && ldecl₁.binderInfo == ldecl₂.binderInfo &&
+        ldecl₁.kind == ldecl₂.kind) <&&>
+      exprsEqualUpToIdsCore₁ ldecl₁.type ldecl₂.type
+    | true, true =>
+      pure (namesEqualUpToMacroScopes ldecl₁.userName ldecl₂.userName &&
+            ldecl₁.kind == ldecl₂.kind) <&&>
+      exprsEqualUpToIdsCore₁ ldecl₁.type ldecl₂.type <&&>
+      exprsEqualUpToIdsCore₁ ldecl₁.value ldecl₂.value
     | _, _ => return false
 
   @[specialize]