Documentation

Lean.Meta.Match.Value

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

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 (Lean.Name × Lean.Expr)

Equations

Lean.Meta.isUIntPatLit? v = match v with | Lean.Expr.app (Lean.Expr.const (Lean.Name.str typeName "mk" x) x_1 x_2) val x_3 => if (Lean.Meta.isUIntTypeName typeName && Lean.Meta.isFinPatLit val) = true then some (typeName, Lean.Expr.appArg! val) else none | x => none

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

Equations

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

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

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

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)