Documentation

Lean.Meta.Match.Match

def Lean.Meta.Match.assignGoalOf (p : Lean.Meta.Match.Problem) (e : Lean.Expr) :

Lean.MetaM Unit

Equations

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

structure Lean.Meta.Match.State:

Type

used : Std.HashSet Nat
counterExamples : List (List Lean.Meta.Match.Example)

structure Lean.Meta.Match.Unify.Context:

Type

altFVarDecls : List Lean.LocalDecl

structure Lean.Meta.Match.Unify.State:

Type

fvarSubst : Lean.Meta.FVarSubst

@[inline]

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

Type

Equations

Lean.Meta.Match.Unify.M = ReaderT Lean.Meta.Match.Unify.Context (StateRefT' IO.RealWorld Lean.Meta.Match.Unify.State Lean.MetaM)

def Lean.Meta.Match.Unify.isAltVar (fvarId : Lean.FVarId) :

Lean.Meta.Match.Unify.M Bool

Equations

Lean.Meta.Match.Unify.isAltVar fvarId = do let a ← read pure (Lean.Meta.Match.inLocalDecls a.altFVarDecls fvarId)

def Lean.Meta.Match.Unify.expandIfVar (e : Lean.Expr) :

Lean.Meta.Match.Unify.M Lean.Expr

Equations

Lean.Meta.Match.Unify.expandIfVar e = match e with | Lean.Expr.fvar a a_1 => do let a ← get pure (Lean.Meta.FVarSubst.apply a.fvarSubst e) | x => pure e

def Lean.Meta.Match.Unify.occurs (fvarId : Lean.FVarId) (v : Lean.Expr) :

Equations

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

def Lean.Meta.Match.Unify.assign (fvarId : Lean.FVarId) (v : Lean.Expr) :

Lean.Meta.Match.Unify.M Bool

Equations

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

partial def Lean.Meta.Match.Unify.unify (a : Lean.Expr) (b : Lean.Expr) :

Lean.Meta.Match.Unify.M Bool

def Lean.Meta.Match.processInaccessibleAsCtor (alt : Lean.Meta.Match.Alt) (ctorName : Lean.Name) :

Lean.MetaM (Option Lean.Meta.Match.Alt)

Equations

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

def Lean.Meta.Match.isCurrVarInductive (p : Lean.Meta.Match.Problem) :

Lean.MetaM Bool

Equations

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

opaque Lean.Meta.Match.bootstrap.genMatcherCode:

Lean.Option Bool

opaque Lean.Meta.Match.matcherExt:

Lean.EnvExtension (Std.PHashMap (Lean.Expr × Bool) Lean.Name)

def Lean.Meta.Match.mkMatcherAuxDefinition (name : Lean.Name) (type : Lean.Expr) (value : Lean.Expr) :

Lean.MetaM (Lean.Expr × Option (Lean.Meta.MatcherInfo → Lean.MetaM Unit))

Equations

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

structure Lean.Meta.Match.MkMatcherInput:

Type

matcherName : Lean.Name
matchType : Lean.Expr
discrInfos : Array Lean.Meta.Match.DiscrInfo
lhss : List Lean.Meta.Match.AltLHS

def Lean.Meta.Match.MkMatcherInput.numDiscrs (m : Lean.Meta.Match.MkMatcherInput) :

Equations

Lean.Meta.Match.MkMatcherInput.numDiscrs m = Array.size m.discrInfos

def Lean.Meta.Match.MkMatcherInput.collectFVars (m : Lean.Meta.Match.MkMatcherInput) :

StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit

Equations

Lean.Meta.Match.MkMatcherInput.collectFVars m = do Lean.Expr.collectFVars m.matchType List.forM m.lhss fun alt => Lean.Meta.Match.AltLHS.collectFVars alt

def Lean.Meta.Match.MkMatcherInput.collectDependencies (m : Lean.Meta.Match.MkMatcherInput) :

Lean.MetaM Lean.FVarIdSet

Equations

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

def Lean.Meta.Match.withCleanLCtxFor {α : Type} (m : Lean.Meta.Match.MkMatcherInput) (k : Lean.MetaM α) :

Auxiliary method used at mkMatcher. It executes k in a local context that contains only the local declarations m depends on. This is important because otherwise dependent elimination may "refine" the types of unnecessary declarations and accidentally introduce unnecessary dependencies in the auto-generated auxiliary declaration. Note that this is not just an optimization because the unnecessary dependencies may prevent the termination checker from succeeding. For an example, see issue #1237.

Equations

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

def Lean.Meta.Match.mkMatcher (input : Lean.Meta.Match.MkMatcherInput) :

Lean.MetaM Lean.Meta.Match.MatcherResult

Create a dependent matcher for matchType where matchType is of the form (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> B[a_1, ..., a_n] where n = numDiscrs, and the lhss are the left-hand-sides of the match-expression alternatives. Each AltLHS has a list of local declarations and a list of patterns. The number of patterns must be the same in each AltLHS. The generated matcher has the structure described at MatcherInfo. The motive argument is of the form (motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v) where v is a universe parameter or 0 if B[a_1, ..., a_n] is a proposition.

Equations

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

def Lean.Meta.Match.getMkMatcherInputInContext (matcherApp : Lean.Meta.MatcherApp) :

Lean.MetaM Lean.Meta.Match.MkMatcherInput

Equations

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

def Lean.Meta.Match.withMkMatcherInput {α : Type} (matcherName : Lean.Name) (k : Lean.Meta.Match.MkMatcherInput → Lean.MetaM α) :

Equations

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

def Lean.Meta.MatcherApp.addArg (matcherApp : Lean.Meta.MatcherApp) (e : Lean.Expr) :

Lean.MetaM Lean.Meta.MatcherApp

Equations

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

def Lean.Meta.MatcherApp.addArg? (matcherApp : Lean.Meta.MatcherApp) (e : Lean.Expr) :

Lean.MetaM (Option Lean.Meta.MatcherApp)

Similar MatcherApp.addArg?, but returns none on failure.

Equations

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