From 710d485e53dcd44faa4902af9bcaf58bb3118c53 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 21 Feb 2024 15:56:55 +1100 Subject: [PATCH 1/2] chore: remove mkAppN macro in omega --- src/Lean/Elab/Tactic/Omega/Frontend.lean | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean index 4ed9fb67ddb4..303bb8f35d4b 100644 --- a/src/Lean/Elab/Tactic/Omega/Frontend.lean +++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean @@ -76,12 +76,6 @@ def mkAtomLinearCombo (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × HashSet let (n, facts) ← lookup e return ⟨LinearCombo.coordinate n, mkCoordinateEvalAtomsEq e n, facts.getD ∅⟩ --- This has been PR'd as --- https://github.com/leanprover/lean4/pull/2900 --- and can be removed when that is merged. -@[inherit_doc mkAppN] -local macro_rules - | `(mkAppN $f #[$xs,*]) => (xs.getElems.foldlM (fun x e => `(Expr.app $x $e)) f : MacroM Term) mutual @@ -221,7 +215,7 @@ partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × | (``HDiv.hDiv, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_ediv []) a b) | (``OfNat.ofNat, #[_, n, _]) => rewrite e (.app (.const ``Int.natCast_ofNat []) n) | (``HMod.hMod, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_emod []) a b) - | (``HSub.hSub, #[_, _, _, _, mkAppN (.const ``HSub.hSub _) #[_, _, _, _, a, b], c]) => + | (``HSub.hSub, #[_, _, _, _, mkApp6 (.const ``HSub.hSub _) _ _ _ _ a b, c]) => rewrite e (mkApp3 (.const ``Int.ofNat_sub_sub []) a b c) | (``Prod.fst, #[_, β, p]) => match p with | .app (.app (.app (.app (.const ``Prod.mk [0, v]) _) _) x) y => From 43fe815f7a8402b272766c81bec4b8ecb124eef4 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 21 Feb 2024 15:57:29 +1100 Subject: [PATCH 2/2] . --- src/Lean/Elab/Tactic/Omega/Frontend.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean index 303bb8f35d4b..c156cb50f8de 100644 --- a/src/Lean/Elab/Tactic/Omega/Frontend.lean +++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean @@ -76,7 +76,6 @@ def mkAtomLinearCombo (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × HashSet let (n, facts) ← lookup e return ⟨LinearCombo.coordinate n, mkCoordinateEvalAtomsEq e n, facts.getD ∅⟩ - mutual /--