Documentation

Lean.Meta.Match.Value

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.
Instances For

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

    Equations
    Instances For

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

      Equations
      Instances For