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
    • One or more equations did not get rendered due to their size.
    Instances For
      @[inline]
      def Char.reduceBinPred (declName : Lean.Name) (arity : Nat) (op : CharCharBool) (e : Lean.Expr) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[inline]
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            Instances For
              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
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For