Documentation

Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char

Return some c if e is a Char.ofNat-application that encodes the character c.

Equations
    Instances For
      @[inline]
      def Char.reduceUnary {α : Type u_1} [Lean.ToExpr α] (declName : Lean.Name) (op : Charα) (arity : Nat := 1) (e : Lean.Expr) :
      Equations
        Instances For
          @[inline]
          def Char.reduceBinPred (declName : Lean.Name) (arity : Nat) (op : CharCharBool) (e : Lean.Expr) :
          Equations
            Instances For
              @[inline]
              Equations
                Instances For
                  Equations
                    Instances For
                      Equations
                        Instances For
                          Equations
                            Instances For
                              Equations
                                Instances For
                                  Equations
                                    Instances For
                                      Equations
                                        Instances For

                                          Returns .done for Char values.

                                          These values should not be unfolded in the symbolic evaluator.

                                          In regular simp, the nested raw literal should be prevented from being converted into an OfNat.ofNat application.

                                          Equations
                                            Instances For