Documentation

Lean.Meta.Tactic.Simp.Arith.Nat.Basic

source
def Nat.Internal.Linear.Expr.applyPerm (perm : Lean.Perm) (e : Expr) :
Expr

Applies the given variable permutation to e

Instances For
    source
    def Nat.Internal.Linear.ExprCnstr.applyPerm (perm : Lean.Perm) :
    ExprCnstr → ExprCnstr

    Applies the given variable permutation to the given expression constraint.

    Instances For
      source
      @[instance_reducible]
      instance Lean.Meta.Simp.Arith.Nat.instReprExpr_lean :
      Repr Nat.Internal.Linear.Expr
      source
      def Lean.Meta.Simp.Arith.Nat.instReprExpr_lean.repr :
      Nat.Internal.Linear.Expr → Nat → Format
      Instances For
        source
        @[instance_reducible]
        instance Lean.Meta.Simp.Arith.Nat.instReprExprCnstr_lean :
        Repr Nat.Internal.Linear.ExprCnstr
        source
        def Lean.Meta.Simp.Arith.Nat.instReprExprCnstr_lean.repr :
        Nat.Internal.Linear.ExprCnstr → Nat → Format
        Instances For
          source
          @[instance_reducible]
          instance Lean.Meta.Simp.Arith.Nat.instReprPolyCnstr_lean :
          Repr Nat.Internal.Linear.PolyCnstr
          source
          def Lean.Meta.Simp.Arith.Nat.instReprPolyCnstr_lean.repr :
          Nat.Internal.Linear.PolyCnstr → Nat → Format
          Instances For
            source
            @[reducible, inline]
            abbrev Lean.Meta.Simp.Arith.Nat.LinearExpr :
            Type
            Instances For
              source
              @[reducible, inline]
              abbrev Lean.Meta.Simp.Arith.Nat.LinearCnstr :
              Type
              Instances For
                source
                @[reducible, inline]
                abbrev Lean.Meta.Simp.Arith.Nat.PolyExpr :
                Type
                Instances For
                  source
                  def Lean.Meta.Simp.Arith.Nat.LinearExpr.toExpr (e : LinearExpr) :
                  Expr
                  Instances For
                    source
                    @[instance_reducible]
                    instance Lean.Meta.Simp.Arith.Nat.instToExprLinearExpr :
                    ToExpr LinearExpr
                    source
                    def Lean.Meta.Simp.Arith.Nat.LinearCnstr.toExpr (c : LinearCnstr) :
                    Expr
                    Instances For
                      source
                      @[instance_reducible]
                      instance Lean.Meta.Simp.Arith.Nat.instToExprLinearCnstr :
                      ToExpr LinearCnstr
                      source
                      def Lean.Meta.Simp.Arith.Nat.LinearExpr.toArith (ctx : Array Expr) (e : LinearExpr) :
                      MetaM Expr
                      Instances For
                        source
                        def Lean.Meta.Simp.Arith.Nat.LinearCnstr.toArith (ctx : Array Expr) (c : LinearCnstr) :
                        MetaM Expr
                        Instances For
                          source
                          structure Lean.Meta.Simp.Arith.Nat.ToLinear.State :
                          Type
                          Instances For
                            source
                            @[reducible, inline]
                            abbrev Lean.Meta.Simp.Arith.Nat.ToLinear.M (α : Type) :
                            Type
                            Instances For
                              source
                              def Lean.Meta.Simp.Arith.Nat.ToLinear.addAsVar (e : Expr) :
                              M LinearExpr
                              Instances For
                                source
                                partial def Lean.Meta.Simp.Arith.Nat.ToLinear.toLinearExpr (e : Expr) :
                                M LinearExpr
                                source
                                def Lean.Meta.Simp.Arith.Nat.ToLinear.toLinearCnstr? (e : Expr) :
                                M (Option LinearCnstr)
                                Instances For
                                  source
                                  def Lean.Meta.Simp.Arith.Nat.ToLinear.run {α : Type} (x : M α) :
                                  MetaM (α × Array Expr)
                                  Instances For
                                    source
                                    def Lean.Meta.Simp.Arith.Nat.toLinearExpr (e : Expr) :
                                    MetaM (LinearExpr × Array Expr)
                                    Instances For
                                      source
                                      def Lean.Meta.Simp.Arith.Nat.toLinearCnstr? (e : Expr) :
                                      MetaM (Option (LinearCnstr × Array Expr))
                                      Instances For
                                        source
                                        def Lean.Meta.Simp.Arith.Nat.toContextExpr (ctx : Array Expr) :
                                        MetaM Expr
                                        Instances For