Reification of arithmetic expressions

Converts Lean expressions into CommRing.Expr (ring) or CommSemiring.Expr (semiring) for reflection-based normalization.

Instance validation uses pointer equality (isSameExpr) against cached function expressions from Functions.lean.

Differences from grind's Reify.lean

• Uses MonadMkVar for variable creation instead of grind's internalize + mkVarCore
• Uses Sym.getNatValue?/Sym.getIntValue? (pure) instead of MetaM versions
• No MonadSetTermId — term-to-ring-id tracking is grind-specific

def Lean.Meta.Sym.Arith.isAddInst {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Sym.Arith.isAddInst inst = do let __do_lift ← Lean.Meta.Sym.Arith.getAddFn pure (Lean.Meta.Sym.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Sym.Arith.isMulInst {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Sym.Arith.isMulInst inst = do let __do_lift ← Lean.Meta.Sym.Arith.getMulFn pure (Lean.Meta.Sym.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Sym.Arith.isSubInst {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Sym.Arith.isSubInst inst = do let __do_lift ← Lean.Meta.Sym.Arith.getSubFn pure (Lean.Meta.Sym.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Sym.Arith.isNegInst {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Sym.Arith.isNegInst inst = do let __do_lift ← Lean.Meta.Sym.Arith.getNegFn pure (Lean.Meta.Sym.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Sym.Arith.isPowInst {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Sym.Arith.isPowInst inst = do let __do_lift ← Lean.Meta.Sym.Arith.getPowFn pure (Lean.Meta.Sym.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Sym.Arith.isIntCastInst {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Sym.Arith.isIntCastInst inst = do let __do_lift ← Lean.Meta.Sym.Arith.getIntCastFn pure (Lean.Meta.Sym.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Sym.Arith.isNatCastInst {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] (inst : Expr) : m Bool

Equations

• Lean.Meta.Sym.Arith.isNatCastInst inst = do let __do_lift ← Lean.Meta.Sym.Arith.getNatCastFn pure (Lean.Meta.Sym.isSameExpr __do_lift.appArg! inst)

def Lean.Meta.Sym.Arith.reifyRing? {m : Type → Type} [MonadLiftT SymM m] [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] [MonadMkVar m] (e : Expr) (skipVar : Bool := true) : m (Option RingExpr)

Converts a Lean expression e into a RingExpr.

If skipVar is true, returns none if e is not an interpreted ring term (used for equalities/disequalities). If false, treats non-interpreted terms as variables (used for inequalities).

Equations

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

def Lean.Meta.Sym.Arith.reifySemiring? {m : Type → Type} [MonadLiftT SymM m] [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] [MonadMkVar m] (e : Expr) : m (Option SemiringExpr)

Converts a Lean expression e into a SemiringExpr. Only recognizes add, mul, pow, natCast, and numerals (no sub, neg, intCast).

Equations

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