From a3cd091efc6838408e54ab11b25886abce372e84 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Thu, 23 Jan 2025 12:47:42 +0000 Subject: [PATCH] rollback unneeded changes to AC/main --- src/Lean/Meta/Tactic/AC/Main.lean | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean index b59e020dbbed..a047a785b228 100644 --- a/src/Lean/Meta/Tactic/AC/Main.lean +++ b/src/Lean/Meta/Tactic/AC/Main.lean @@ -56,8 +56,6 @@ def preContext (expr : Expr) : MetaM (Option PreContext) := do return none - - inductive PreExpr | op (lhs rhs : PreExpr) | var (e : Expr) @@ -88,20 +86,6 @@ def toACExpr (op l r : Expr) : MetaM (Array Expr × ACExpr) := do | PreExpr.op l r => Data.AC.Expr.op (toACExpr varMap l) (toACExpr varMap r) | PreExpr.var x => Data.AC.Expr.var (varMap x) -/-- -Compute a map from variable index to the number of occurences of that variable -in the given expression --/ -def ACExpr.coefficients : ACExpr → Std.HashMap Nat Nat := - go {} - where go (map : Std.HashMap Nat Nat) - | .var idx => map.alter idx (fun - | some cnt => some (cnt + 1) - | none => some 0) - | .op lhs rhs => - let map := go map lhs - go map rhs - /-- In order to prevent the kernel trying to reduce the atoms of the expression, we abstract the proof over them. But `ac_rfl` proofs are not completely abstract in the value of the atoms – it recognizes