Documentation

Lean.Meta.Match.Basic

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) :

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: Lean.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

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

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
idx : Nat
rhs : Lean.Expr
fvarDecls : List Lean.LocalDecl
patterns : List Lean.Meta.Match.Pattern

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 } }

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.checkAndReplaceFVarId (fvarId : Lean.FVarId) (v : Lean.Expr) (alt : Lean.Meta.Match.Alt) :

Lean.MetaM Lean.Meta.Match.Alt

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: Lean.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

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 α) :

Equations

Lean.Meta.Match.withGoalOf p x = Lean.Meta.withMVarContext 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]

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