diff --git a/Export.lean b/Export.lean index 7a73832..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.updateLet! (← 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 => 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