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

Equations

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

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

Equations

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

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

Equations

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

inductive Lean.Meta.Match.Pattern : Type

• inaccessible: Lean.Expr → Lean.Meta.Match.Pattern
• var: Lean.FVarId → Lean.Meta.Match.Pattern
• ctor: Lake.Name → List Lean.Level → List Lean.Expr → List Lean.Meta.Match.Pattern → Lean.Meta.Match.Pattern
• val: Lean.Expr → Lean.Meta.Match.Pattern
• arrayLit: Lean.Expr → List Lean.Meta.Match.Pattern → Lean.Meta.Match.Pattern
• as: Lean.FVarId → Lean.Meta.Match.Pattern → Lean.FVarId → Lean.Meta.Match.Pattern

instance Lean.Meta.Match.instInhabitedPattern : Inhabited Lean.Meta.Match.Pattern

Equations

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

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

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

Equations

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

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

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

Apply the free variable substitution s to the given pattern

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

Equations

• Lean.Meta.Match.Pattern.replaceFVarId fvarId v p = let s := { map := ∅ }; Lean.Meta.Match.Pattern.applyFVarSubst (Lean.Meta.FVarSubst.insert s fvarId v) p

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

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

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

structure Lean.Meta.Match.AltLHS : Type

• ref : Lean.Syntax
• fvarDecls : List Lean.LocalDecl
• patterns : List Lean.Meta.Match.Pattern

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

Equations

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

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

Equations

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

structure Lean.Meta.Match.Alt : Type

• ref : Lean.Syntax

  Syntax object for providing position information

• idx : Nat

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

• rhs : Lean.Expr

  Right-hand-side of the alternative.

• fvarDecls : List Lean.LocalDecl

  Alternative pattern variables.

• patterns : List Lean.Meta.Match.Pattern

  Alternative patterns.

• cnstrs : List (Lean.Expr × Lean.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.

Match alternative

instance Lean.Meta.Match.instInhabitedAlt : Inhabited Lean.Meta.Match.Alt

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Return true if fvarId is one of the alternative pattern variables

Equations

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

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

Similar to checkAndReplaceFVarId, but ensures type of v is definitionally equal to type of fvarId. This extra check is necessary when performing dependent elimination and inaccessible terms have been used. For example, consider the following code fragment:

inductive Vec (α : Type u) : Nat → Type u where
  | nil : Vec α 0
  | cons {n} (head : α) (tail : Vec α n) : Vec α (n+1)

inductive VecPred {α : Type u} (P : α → Prop) : {n : Nat} → Vec α n → Prop where
  | nil   : VecPred P Vec.nil
  | cons  {n : Nat} {head : α} {tail : Vec α n} : P head → VecPred P tail → VecPred P (Vec.cons head tail)

theorem ex {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
  | _, Vec.cons head _, VecPred.cons h (w : VecPred P Vec.nil) => ⟨head, h⟩

Recall that _ in a pattern can be elaborated into pattern variable or an inaccessible term. The elaborator uses an inaccessible term when typing constraints restrict its value. Thus, in the example above, the _ at Vec.cons head _ becomes the inaccessible pattern .(Vec.nil) because the type ascription (w : VecPred P Vec.nil) propagates typing constraints that restrict its value to be Vec.nil. After elaboration the alternative becomes:

  | .(0), @Vec.cons .(α) .(0) head .(Vec.nil), @VecPred.cons .(α) .(P) .(0) .(head) .(Vec.nil) h w => ⟨head, h⟩

where

(head : α), (h: P head), (w : VecPred P Vec.nil)

Then, when we process this alternative in this module, the following check will detect that w has type VecPred P Vec.nil, when it is supposed to have type VecPred P tail. Note that if we had written

theorem ex {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
  | _, Vec.cons head Vec.nil, VecPred.cons h (w : VecPred P Vec.nil) => ⟨head, h⟩

we would get the easier to digest error message

missing cases:
_, (Vec.cons _ _ (Vec.cons _ _ _)), _

Equations

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

inductive Lean.Meta.Match.Example : Type

• var: Lean.FVarId → Lean.Meta.Match.Example
• underscore: Lean.Meta.Match.Example
• ctor: Lake.Name → List Lean.Meta.Match.Example → Lean.Meta.Match.Example
• val: Lean.Expr → Lean.Meta.Match.Example
• arrayLit: List Lean.Meta.Match.Example → Lean.Meta.Match.Example

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

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

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

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

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

Equations

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

structure Lean.Meta.Match.Problem : Type

• mvarId : Lean.MVarId
• vars : List Lean.Expr
• alts : List Lean.Meta.Match.Alt
• examples : List Lean.Meta.Match.Example

instance Lean.Meta.Match.instInhabitedProblem : Inhabited Lean.Meta.Match.Problem

Equations

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

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

Equations

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

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

Equations

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

@[inline, reducible]

abbrev Lean.Meta.Match.CounterExample : Type

Equations

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

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

Equations

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

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

Equations

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

structure Lean.Meta.Match.MatcherResult : Type

• matcher : Lean.Expr
• counterExamples : List Lean.Meta.Match.CounterExample
• unusedAltIdxs : List Nat
• addMatcher : Lean.MetaM Unit

partial def Lean.Meta.Match.toPattern (e : Lean.Expr) : Lean.MetaM Lean.Meta.Match.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