sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

fix: remove accidentally added code from Sym.Simp.Pattern (#12926)

Browse Source 
This PR removes unused functions (`mkPatternCoreFromLambda`,
`mkPatternFromLambda`, `mkSimprocPatternFromExpr`) and the `import
Lean.Meta.AbstractMVars` that were added to `Lean.Meta.Sym.Pattern`
after merging #12597.
This commit is contained in:
Wojciech Różowski
2026-03-15 10:30:26 +00:00
committed by GitHub
parent cfa8c5a036
commit 6631352136
1 changed files with 0 additions and 41 deletions
Download Patch File Download Diff File Expand all files Collapse all files

41
src/Lean/Meta/Sym/Pattern.lean
View File

@@ -18,7 +18,6 @@ import Lean.Meta.Sym.AlphaShareBuilder
import Lean.Meta.Sym.Offset
import Lean.Meta.Sym.Eta
import Lean.Meta.Sym.Util
import Lean.Meta.AbstractMVars
import Init.Data.List.MapIdx
import Init.Data.Nat.Linear
import Std.Do.Triple.Basic
@@ -266,46 +265,6 @@ public def mkEqPatternFromDecl (declName : Name) : MetaM (Pattern × Expr) := do
let_expr Eq _ lhs rhs := type | throwError "conclusion is not a equality{indentExpr type}"
return (lhs, rhs)
/--
Like `mkPatternCore` but takes a lambda expression instead of a forall type.
Uses `lambdaBoundedTelescope` to open binders and detect instance/proof arguments.
-/
def mkPatternCoreFromLambda (lam : Expr) (levelParams : List Name)
(varTypes : Array Expr) (pattern : Expr) : MetaM Pattern := do
let fnInfos ← mkProofInstInfoMapFor pattern
let checkTypeMask := mkCheckTypeMask pattern varTypes.size
let checkTypeMask? := if checkTypeMask.all (· == false) then none else some checkTypeMask
let varInfos? ← lambdaBoundedTelescope lam varTypes.size fun xs _ =>
mkProofInstArgInfo? xs
return { levelParams, varTypes, pattern, fnInfos, varInfos?, checkTypeMask? }
def mkPatternFromLambda (levelParams : List Name) (lam : Expr) : MetaM Pattern := do
let rec go (pattern : Expr) (varTypes : Array Expr) : MetaM Pattern := do
if let .lam _ d b _ := pattern then
return (← go b (varTypes.push d))
let pattern ← preprocessType pattern
mkPatternCoreFromLambda lam levelParams varTypes pattern
go lam #[]
/--
Creates a `Pattern` from an expression containing metavariables.
Metavariables in `e` become pattern variables (wildcards). For example,
`Nat.succ ?m` produces a pattern matching `Nat.succ _` with discrimination
tree keys `[Nat.succ, *]`.
This is used for user-registered simproc patterns where the user provides
an expression with underscores (elaborated as metavariables) to specify
what the simproc should match.
-/
public def mkSimprocPatternFromExpr (e : Expr) : MetaM Pattern := do
let result ← abstractMVars e
let levelParams := result.paramNames.mapIdx fun i _ => Name.num uvarPrefix i
let us := levelParams.toList.map mkLevelParam
let expr := result.expr.instantiateLevelParamsArray result.paramNames us.toArray
let expr ← normalizeLevels expr
mkPatternFromLambda levelParams.toList expr
structure UnifyM.Context where
pattern : Pattern
unify : Bool := true