From 946a278706e7c19f4769ee0f7d403bbec36a78ef Mon Sep 17 00:00:00 2001 From: ammkrn Date: Tue, 8 Jul 2025 11:50:55 -0700 Subject: [PATCH 1/2] chore: adaptations for v4.22.0-rc3 --- Export.lean | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Export.lean b/Export.lean index 7a73832..4827ecb 100644 --- a/Export.lean +++ b/Export.lean @@ -78,7 +78,7 @@ def removeMData (e : Expr) : M Expr := do | .lam _ d b _ => pure <| e.updateLambdaE! (← removeMData d) (← removeMData b) | .letE _ d v b _ => - pure <| e.updateLet! (← removeMData d) (← removeMData v) (← removeMData b) + pure <| e.updateLetE! (← removeMData d) (← removeMData v) (← removeMData b) | .forallE _ d b _ => pure <| e.updateForallE! (← removeMData d) (← removeMData b) | .proj _ _ e2 => diff --git a/lean-toolchain b/lean-toolchain index 1efd365..fff0a20 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.21.0-rc3 +leanprover/lean4:v4.22.0-rc3 From eb023e55e0852a9bf9b569ecefc42d54338b0c8f Mon Sep 17 00:00:00 2001 From: ammkrn Date: Tue, 22 Jul 2025 20:05:27 -0700 Subject: [PATCH 2/2] fix: normalize `nondep` flag for `letE` exprs The BEq implementation for Expr checks the `nondep` flag, but `nondep` does not exist as far as type checkers are concerned, so we also need to normalize these in order prevent export of duplicate expressions with different indices. --- Export.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Export.lean b/Export.lean index 4827ecb..12459e1 100644 --- a/Export.lean +++ b/Export.lean @@ -78,7 +78,7 @@ def removeMData (e : Expr) : M Expr := do | .lam _ d b _ => pure <| e.updateLambdaE! (← removeMData d) (← removeMData b) | .letE _ d v b _ => - pure <| e.updateLetE! (← removeMData d) (← removeMData v) (← removeMData b) + pure <| e.updateLet! (← removeMData d) (← removeMData v) (← removeMData b) false | .forallE _ d b _ => pure <| e.updateForallE! (← removeMData d) (← removeMData b) | .proj _ _ e2 =>