From 6719af350fde9339354f28d091458df39a4af9d4 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 21 Feb 2024 16:11:37 +1100 Subject: [PATCH] chore: remove mkAppN macro in omega (#3428) --- src/Lean/Elab/Tactic/Omega/Frontend.lean | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean index 4ed9fb67ddb4..c156cb50f8de 100644 --- a/src/Lean/Elab/Tactic/Omega/Frontend.lean +++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean @@ -76,13 +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 +214,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 =>