structure Blaster.Optimize.MatcherRecInfo : Type

• mInfo : Lean.Meta.MatcherInfo

  MatcherInfo for match

• isCasesOn : Bool

  Flag set to true only when match is a casesOn -

instance Blaster.Optimize.instReprMatcherInfo_blaster : Repr Lean.Meta.MatcherInfo

Equations

• Blaster.Optimize.instReprMatcherInfo_blaster = { reprPrec := fun (x : Lean.Meta.MatcherInfo) (x : Nat) => Std.Format.text "<MatcherInfo>" }

instance Blaster.Optimize.instReprMatcherRecInfo : Repr MatcherRecInfo

Equations

• Blaster.Optimize.instReprMatcherRecInfo = { reprPrec := fun (x : Blaster.Optimize.MatcherRecInfo) (x : Nat) => Std.Format.text "<MatcherRecInfo>" }

structure Blaster.Optimize.MatchInfo : Type

• name : Lean.Name

  Name of match

• nameExpr : Lean.Expr

  Name expression of match

• instApp : Lean.Expr

  match generic optimized instance (see InitOptimizeMatchInfo case)

• recInfo : MatcherRecInfo

  MatcherInfo for match

instance Blaster.Optimize.instReprMatchInfo : Repr MatchInfo

Equations

• Blaster.Optimize.instReprMatchInfo = { reprPrec := Blaster.Optimize.instReprMatchInfo.repr }

def Blaster.Optimize.instReprMatchInfo.repr : MatchInfo → Nat → Std.Format

Equations

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

@[inline]

def Blaster.Optimize.MatchInfo.numParams (minfo : MatchInfo) : Nat

Equations

• minfo.numParams = minfo.recInfo.mInfo.numParams

@[inline]

def Blaster.Optimize.MatchInfo.numAlts (minfo : MatchInfo) : Nat

Equations

• minfo.numAlts = minfo.recInfo.mInfo.altNumParams.size

@[inline]

def Blaster.Optimize.MatchInfo.numDiscrs (minfo : MatchInfo) : Nat

Equations

• minfo.numDiscrs = minfo.recInfo.mInfo.numDiscrs

@[inline]

def Blaster.Optimize.MatchInfo.arity (minfo : MatchInfo) : Nat

Equations

• minfo.arity = minfo.numParams + 1 + minfo.numDiscrs + minfo.numAlts

@[inline]

def Blaster.Optimize.MatchInfo.getFirstDiscrPos (info : MatchInfo) : Nat

Equations

• info.getFirstDiscrPos = info.numParams + 1

@[inline]

def Blaster.Optimize.MatchInfo.getDiscrRange (info : MatchInfo) : Std.Range

Equations

• info.getDiscrRange = [info.getFirstDiscrPos:info.getFirstDiscrPos + info.numDiscrs]

@[inline]

def Blaster.Optimize.MatchInfo.getFirstAltPos (info : MatchInfo) : Nat

Equations

• info.getFirstAltPos = info.numParams + 1 + info.numDiscrs

@[inline]

def Blaster.Optimize.MatchInfo.isCasesOn (info : MatchInfo) : Bool

Equations

• info.isCasesOn = info.recInfo.isCasesOn