Documentation

Lean.Meta.Match.MatchEqs

def Lean.Meta.casesOnStuckLHS (mvarId : Lean.MVarId) :

Lean.MetaM (Array Lean.MVarId)

Equations

Lean.Meta.casesOnStuckLHS mvarId = (fun findFVar? => do let target ← Lean.Meta.getMVarType mvarId let a ← Lean.Meta.matchEq? target let _do_jp : PUnit → Lean.MetaM (Array Lean.MVarId) := fun y => Lean.throwError (Lean.toMessageData "'casesOnStuckLHS' failed") match a with | some (x, lhs, rhs) => do let a ← findFVar? lhs match a with | some fvarId => do let a ← Lean.Meta.cases mvarId fvarId #[] pure (Array.map (fun s => s.toInductionSubgoal.mvarId) a) | x => do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y) Lean.Meta.casesOnStuckLHS.findFVar?

partial def Lean.Meta.casesOnStuckLHS.findFVar? (e : Lean.Expr) :

Lean.MetaM (Option Lean.FVarId)

def Lean.Meta.casesOnStuckLHS? (mvarId : Lean.MVarId) :

Lean.MetaM (Option (Array Lean.MVarId))

Equations

Lean.Meta.casesOnStuckLHS? mvarId = do let r ← tryCatch (do let y ← Lean.Meta.casesOnStuckLHS mvarId pure (DoResultPR.pure y PUnit.unit)) fun x => pure (DoResultPR.return none PUnit.unit) match r with | DoResultPR.pure a u => let x := u; pure (some a) | DoResultPR.return b u => let x := u; pure b

structure Lean.Meta.Match.MatchEqns :

Type

eqnNames : Array Lean.Name
splitterName : Lean.Name
splitterAltNumParams : Array Nat

instance Lean.Meta.Match.instInhabitedMatchEqns :

Inhabited Lean.Meta.Match.MatchEqns

Equations

Lean.Meta.Match.instInhabitedMatchEqns = { default := { eqnNames := default, splitterName := default, splitterAltNumParams := default } }

instance Lean.Meta.Match.instReprMatchEqns :

Repr Lean.Meta.Match.MatchEqns

Equations

Lean.Meta.Match.instReprMatchEqns = { reprPrec := [anonymous] }

structure Lean.Meta.Match.MatchEqnsExtState :

Type

map : Std.PHashMap Lean.Name Lean.Meta.Match.MatchEqns

instance Lean.Meta.Match.instInhabitedMatchEqnsExtState :

Inhabited Lean.Meta.Match.MatchEqnsExtState

Equations

Lean.Meta.Match.instInhabitedMatchEqnsExtState = { default := { map := default } }

constant Lean.Meta.Match.matchEqnsExt :

Lean.EnvExtension Lean.Meta.Match.MatchEqnsExtState

def Lean.Meta.Match.unfoldNamedPattern (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.Match.unfoldNamedPattern e = let visit := fun e => let _do_jp := fun y => pure (Lean.TransformStep.visit e); if Lean.Expr.isAppOfArity e `namedPattern 4 = true then do let a ← Lean.Meta.unfoldDefinition? e match a with | some eNew => pure (Lean.TransformStep.visit eNew) | x => do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y; Lean.Meta.transform e visit fun e => pure (Lean.TransformStep.done e)

def Lean.Meta.Match.forallAltTelescope {α : Type} (altType : Lean.Expr) (k : Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.Expr → Lean.MetaM α) :

Equations

Lean.Meta.Match.forallAltTelescope altType k = (fun go isNamedPatternProof => go #[] #[] #[] altType) (Lean.Meta.Match.forallAltTelescope.go k) Lean.Meta.Match.forallAltTelescope.isNamedPatternProof

partial def Lean.Meta.Match.forallAltTelescope.go {α : Type} (k : Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.Expr → Lean.MetaM α) (ys : Array Lean.Expr) (args : Array Lean.Expr) (mask : Array Bool) (type : Lean.Expr) :

def Lean.Meta.Match.forallAltTelescope.isNamedPatternProof (type : Lean.Expr) (h : Lean.Expr) :

Equations

Lean.Meta.Match.forallAltTelescope.isNamedPatternProof type h = Option.isSome (Lean.Expr.find? (fun e => Lean.Expr.isAppOfArity e `namedPattern 4 && Lean.Expr.appArg! e == h) type)

structure Lean.Meta.Match.SimpH.State :

Type

mvarId : Lean.MVarId
xs : List Lean.FVarId
eqs : List Lean.FVarId
eqsNew : List Lean.FVarId

@[inline]

abbrev Lean.Meta.Match.SimpH.M (α : Type) :

Type

Equations

Lean.Meta.Match.SimpH.M = StateRefT' IO.RealWorld Lean.Meta.Match.SimpH.State Lean.MetaM

partial def Lean.Meta.Match.SimpH.go :

Lean.Meta.Match.SimpH.M Bool

def Lean.Meta.Match.proveCondEqThm (matchDeclName : Lean.Name) (type : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.Match.proveCondEqThm matchDeclName type = (fun go => do let type ← Lean.Meta.instantiateMVars type Lean.Meta.withLCtx { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } ∅ (Lean.Meta.forallTelescope type fun ys target => do let mvar0 ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar target Lean.Name.anonymous let mvarId ← Lean.Meta.deltaTarget (Lean.Expr.mvarId! mvar0) fun a => a == matchDeclName let cls : Lean.Name := `Meta.Match.matchEqs let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Expr := fun y => do Lean.Meta.withDefault (go mvarId 0) let a ← Lean.Meta.instantiateMVars mvar0 Lean.Meta.mkLambdaFVars ys a false true if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData (Lean.MessageData.ofGoal mvarId) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y)) Lean.Meta.Match.proveCondEqThm.go

partial def Lean.Meta.Match.proveCondEqThm.go (mvarId : Lean.MVarId) (depth : Nat) :

Lean.MetaM Unit

inductive Lean.Meta.Match.InjectionAnyResult :

Type

solved: Lean.Meta.Match.InjectionAnyResult
failed: Lean.Meta.Match.InjectionAnyResult
subgoal: Lean.MVarId → Lean.Meta.Match.InjectionAnyResult

def Lean.Meta.Match.getEquationsFor (matchDeclName : Lean.Name) :

Lean.MetaM Lean.Meta.Match.MatchEqns

Equations

Lean.Meta.Match.getEquationsFor matchDeclName = do let a ← Lean.getEnv match Std.PersistentHashMap.find? (Lean.EnvExtension.getState Lean.Meta.Match.matchEqnsExt a).map matchDeclName with | some matchEqns => pure matchEqns | none => Lean.Meta.Match.mkEquationsFor matchDeclName