def Lean.Meta.Match.mkNamedPattern (x h p : Expr) : MetaM Expr

Equations

• Lean.Meta.Match.mkNamedPattern x h p = Lean.Meta.mkAppM `namedPattern #[x, p, h]

def Lean.Meta.Match.isNamedPattern (e : Expr) : Bool

Equations

• Lean.Meta.Match.isNamedPattern e = (e.consumeMData.getAppNumArgs == 4 && e.consumeMData.getAppFn.consumeMData.isConstOf `namedPattern)

def Lean.Meta.Match.isNamedPattern? (e : Expr) : Option Expr

Equations

• Lean.Meta.Match.isNamedPattern? e = if (e.consumeMData.getAppNumArgs == 4 && e.consumeMData.getAppFn.consumeMData.isConstOf `namedPattern) = true then some e.consumeMData else none

inductive Lean.Meta.Match.Pattern : Type

• inaccessible (e : Expr) : Pattern
• var (fvarId : FVarId) : Pattern
• ctor (ctorName : Name) (us : List Level) (params : List Expr) (fields : List Pattern) : Pattern
• val (e : Expr) : Pattern
• arrayLit (type : Expr) (xs : List Pattern) : Pattern
• as (varId : FVarId) (p : Pattern) (hId : FVarId) : Pattern

instance Lean.Meta.Match.instInhabitedPattern : Inhabited Pattern

Equations

• Lean.Meta.Match.instInhabitedPattern = { default := Lean.Meta.Match.instInhabitedPattern.default }

def Lean.Meta.Match.instInhabitedPattern.default : Pattern

Equations

• Lean.Meta.Match.instInhabitedPattern.default = Lean.Meta.Match.Pattern.inaccessible default

partial def Lean.Meta.Match.Pattern.toMessageData : Pattern → MessageData

def Lean.Meta.Match.Pattern.toExpr (p : Pattern) (annotate : Bool := false) : MetaM Expr

Equations

• p.toExpr annotate = Lean.Meta.Match.Pattern.toExpr.visit✝ annotate p

partial def Lean.Meta.Match.Pattern.applyFVarSubst (s : FVarSubst) : Pattern → Pattern

Apply the free variable substitution s to the given pattern

def Lean.Meta.Match.Pattern.replaceFVarId (fvarId : FVarId) (v : Expr) (p : Pattern) : Pattern

Equations

• Lean.Meta.Match.Pattern.replaceFVarId fvarId v p = Lean.Meta.Match.Pattern.applyFVarSubst ({ }.insert fvarId v) p

partial def Lean.Meta.Match.Pattern.hasExprMVar : Pattern → Bool

partial def Lean.Meta.Match.Pattern.collectFVars (p : Pattern) : StateRefT' IO.RealWorld CollectFVars.State MetaM Unit

partial def Lean.Meta.Match.instantiatePatternMVars : Pattern → MetaM Pattern

structure Lean.Meta.Match.AltLHS : Type

• ref : Syntax
• fvarDecls : List LocalDecl
• patterns : List Pattern

instance Lean.Meta.Match.instInhabitedAltLHS : Inhabited AltLHS

Equations

• Lean.Meta.Match.instInhabitedAltLHS = { default := Lean.Meta.Match.instInhabitedAltLHS.default }

def Lean.Meta.Match.instInhabitedAltLHS.default : AltLHS

Equations

• Lean.Meta.Match.instInhabitedAltLHS.default = { ref := default, fvarDecls := default, patterns := default }

def Lean.Meta.Match.AltLHS.collectFVars (altLHS : AltLHS) : StateRefT' IO.RealWorld CollectFVars.State MetaM Unit

Equations

• altLHS.collectFVars = do altLHS.fvarDecls.forM fun (fvarDecl : Lean.LocalDecl) => fvarDecl.collectFVars altLHS.patterns.forM fun (p : Lean.Meta.Match.Pattern) => p.collectFVars

def Lean.Meta.Match.instantiateAltLHSMVars (altLHS : AltLHS) : MetaM AltLHS

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Meta.Match.Alt : Type

Match alternative

• ref : Syntax

  Syntax object for providing position information

• idx : Nat

  Original alternative index. Alternatives can be split, this index is the original position of the alternative that generated this one.

• rhs : Expr

  Right-hand-side of the alternative.

• fvarDecls : List LocalDecl

  Alternative pattern variables.

• patterns : List Pattern

  Alternative patterns.

• cnstrs : List (Expr × Expr)

  Pending constraints lhs ≋ rhs that need to be solved before the alternative is considered acceptable. We generate them when processing inaccessible patterns. Note that lhs and rhs often have different types. After we perform additional case analysis, their types become definitionally equal.

def Lean.Meta.Match.instInhabitedAlt.default : Alt

Equations

• Lean.Meta.Match.instInhabitedAlt.default = { ref := default, idx := default, rhs := default, fvarDecls := default, patterns := default, cnstrs := default }

instance Lean.Meta.Match.instInhabitedAlt : Inhabited Alt

Equations

• Lean.Meta.Match.instInhabitedAlt = { default := Lean.Meta.Match.instInhabitedAlt.default }

def Lean.Meta.Match.Alt.toMessageData (alt : Alt) : MetaM MessageData

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Match.Alt.applyFVarSubst (s : FVarSubst) (alt : Alt) : Alt

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Match.Alt.replaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : Alt

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Match.Alt.isLocalDecl (fvarId : FVarId) (alt : Alt) : Bool

Return true if fvarId is one of the alternative pattern variables

Equations

• Lean.Meta.Match.Alt.isLocalDecl fvarId alt = alt.fvarDecls.any fun (d : Lean.LocalDecl) => d.fvarId == fvarId

inductive Lean.Meta.Match.Example : Type

• var : FVarId → Example
• underscore : Example
• ctor : Name → List Example → Example
• val : Expr → Example
• arrayLit : List Example → Example

partial def Lean.Meta.Match.Example.replaceFVarId (fvarId : FVarId) (ex : Example) : Example → Example

partial def Lean.Meta.Match.Example.applyFVarSubst (s : FVarSubst) : Example → Example

partial def Lean.Meta.Match.Example.varsToUnderscore : Example → Example

partial def Lean.Meta.Match.Example.toMessageData : Example → MessageData

def Lean.Meta.Match.examplesToMessageData (cex : List Example) : MessageData

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Meta.Match.Problem : Type

• mvarId : MVarId
• vars : List Expr
• alts : List Alt
• examples : List Example

instance Lean.Meta.Match.instInhabitedProblem : Inhabited Problem

Equations

• Lean.Meta.Match.instInhabitedProblem = { default := Lean.Meta.Match.instInhabitedProblem.default }

def Lean.Meta.Match.instInhabitedProblem.default : Problem

Equations

• Lean.Meta.Match.instInhabitedProblem.default = { mvarId := default, vars := default, alts := default, examples := default }

def Lean.Meta.Match.withGoalOf {α : Type} (p : Problem) (x : MetaM α) : MetaM α

Equations

• Lean.Meta.Match.withGoalOf p x = p.mvarId.withContext x

def Lean.Meta.Match.Problem.toMessageData (p : Problem) : MetaM MessageData

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Lean.Meta.Match.CounterExample : Type

Equations

• Lean.Meta.Match.CounterExample = List Lean.Meta.Match.Example

def Lean.Meta.Match.counterExampleToMessageData (cex : CounterExample) : MessageData

Equations

• Lean.Meta.Match.counterExampleToMessageData cex = Lean.Meta.Match.examplesToMessageData cex

def Lean.Meta.Match.counterExamplesToMessageData (cexs : List CounterExample) : MessageData

Equations

• Lean.Meta.Match.counterExamplesToMessageData cexs = Lean.MessageData.joinSep (List.map Lean.Meta.Match.counterExampleToMessageData cexs) (Lean.MessageData.ofFormat Std.Format.line)

structure Lean.Meta.Match.MatcherResult : Type

• matcher : Expr
• counterExamples : List CounterExample
• unusedAltIdxs : List Nat
• addMatcher : MetaM Unit

partial def Lean.Meta.Match.toPattern (e : Expr) : MetaM Pattern

Convert a expression occurring as the argument of a match motive application back into a Pattern For example, we can use this method to convert x::y::xs at

...
(motive : List Nat → Sort u_1) (xs : List Nat) (h_1 : (x y : Nat) → (xs : List Nat) → motive (x :: y :: xs))
...

into a pattern object

Match congruence equational theorem names helper declarations and functions

def Lean.Meta.Match.congrEqnThmSuffixBase : String

Equations

• Lean.Meta.Match.congrEqnThmSuffixBase = "congr_eq"

def Lean.Meta.Match.congrEqnThmSuffixBasePrefix : String

Equations

• Lean.Meta.Match.congrEqnThmSuffixBasePrefix = Lean.Meta.Match.congrEqnThmSuffixBase ++ "_"

def Lean.Meta.Match.congrEqn1ThmSuffix : String

Equations

• Lean.Meta.Match.congrEqn1ThmSuffix = Lean.Meta.Match.congrEqnThmSuffixBasePrefix ++ "1"

def Lean.Meta.Match.isCongrEqnReservedNameSuffix (s : String) : Bool

Returns true if s is of the form congr_eq_<idx>

Equations

• Lean.Meta.Match.isCongrEqnReservedNameSuffix s = (Lean.Meta.Match.congrEqnThmSuffixBasePrefix.isPrefixOf s && (s.drop Lean.Meta.Match.congrEqnThmSuffixBasePrefix.length).isNat)