Documentation

Lean.Meta.Match.Value

source
def Lean.Meta.isFinPatLit (e : Lean.Expr) :
Bool
Equations
source
def Lean.Meta.isUIntPatLit? (v : Lean.Expr) :
Option (Lean.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.
source
def Lean.Meta.isUIntPatLit (v : Lean.Expr) :
Bool
Equations
source
def Lean.Meta.foldPatValue (v : Lean.Expr) :
Lean.Expr

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

Equations
source
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