def Lean.Meta.isFinPatLit (e : Lean.Expr) : Bool

Equations

• Lean.Meta.isFinPatLit e = (Lean.Expr.isAppOfArity e `Fin.ofNat 2 && Lean.Expr.isNatLit (Lean.Expr.appArg! e))

def Lean.Meta.isUIntPatLit? (v : Lean.Expr) : Option (Lake.Name × Lean.Expr)

Return some (typeName, numLit) if v is of the form UInt*.mk (Fin.ofNat _ numLit)

Equations

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

def Lean.Meta.isUIntPatLit (v : Lean.Expr) : Bool

Equations

• Lean.Meta.isUIntPatLit v = Option.isSome (Lean.Meta.isUIntPatLit? v)

def Lean.Meta.foldPatValue (v : Lean.Expr) : Lean.Expr

The frontend expands uint numerals occurring in patterns into UInt*.mk .. constructor applications. This method convert them back into UInt*.ofNat .. applications.

Equations

• Lean.Meta.foldPatValue v = match Lean.Meta.isUIntPatLit? v with | some (typeName, numLit) => Lean.mkApp (Lean.mkConst (Lean.Name.mkStr typeName "ofNat")) numLit | x => v

def Lean.Meta.isMatchValue (e : Lean.Expr) : Bool

Return true is e is a term that should be processed by the match-compiler using casesValues

Equations

• Lean.Meta.isMatchValue e = (Lean.Expr.isNatLit e || Lean.Expr.isCharLit e || Lean.Expr.isStringLit e || Lean.Meta.isFinPatLit e || Lean.Meta.isUIntPatLit e)