Documentation

Lean.Meta.LitValues

Helper functions for recognizing builtin literal values. This module focus on recognizing the standard representation used in Lean for these literals. It also provides support for the following exceptional cases.

Returns some n if e is a raw natural number, i.e., it is of the form .lit (.natVal n).

Equations
    Instances For
      def Lean.Meta.getOfNatValue? (e : Expr) (typeDeclName : Name) :

      Return some (n, type) if e is an OfNat.ofNat-application encoding n for a type with name typeDeclName.

      Equations
        Instances For

          Return some n if e is a raw natural number or an OfNat.ofNat-application encoding n.

          Equations
            Instances For

              Return some i if e OfNat.ofNat-application encoding an integer, or Neg.neg-application of one.

              Equations
                Instances For

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

                  Equations
                    Instances For

                      Return some s if e is of the form .lit (.strVal s).

                      Equations
                        Instances For
                          def Lean.Meta.getFinValue? (e : Expr) :
                          MetaM (Option ((n : Nat) × Fin n))

                          Return some ⟨n, v⟩ if e is an OfNat.ofNat application encoding a Fin n with value v

                          Equations
                            Instances For

                              Return some ⟨n, v⟩ if e is:

                              Equations
                                Instances For

                                  Return some n if e is an OfNat.ofNat-application encoding the UInt8 with value n.

                                  Equations
                                    Instances For

                                      Return some n if e is an OfNat.ofNat-application encoding the UInt16 with value n.

                                      Equations
                                        Instances For

                                          Return some n if e is an OfNat.ofNat-application encoding the UInt32 with value n.

                                          Equations
                                            Instances For

                                              Return some n if e is an OfNat.ofNat-application encoding the UInt64 with value n.

                                              Equations
                                                Instances For

                                                  If e is a literal value, ensure it is encoded using the standard representation. Otherwise, just return e.

                                                  Equations
                                                    Instances For

                                                      Returns true if e is a literal value.

                                                      Equations
                                                        Instances For

                                                          If e is a Nat, Int, or Fin literal value, converts it into a constructor application. Otherwise, just return e.

                                                          Equations
                                                            Instances For
                                                              def Lean.Meta.getListLitOf? {α : Type} (e : Expr) (f : ExprMetaM (Option α)) :

                                                              Check if an expression is a list literal (i.e. a nested chain of List.cons, ending at a List.nil), where each element is "recognised" by a given function f : Expr → MetaM (Option α), and return the array of recognised values.

                                                              Equations
                                                                Instances For

                                                                  Check if an expression is a list literal (i.e. a nested chain of List.cons, ending at a List.nil), returning the array of Expr values.

                                                                  Equations
                                                                    Instances For
                                                                      def Lean.Meta.getArrayLitOf? {α : Type} (e : Expr) (f : ExprMetaM (Option α)) :

                                                                      Check if an expression is an array literal (i.e. List.toArray applied to a nested chain of List.cons, ending at a List.nil), where each element is "recognised" by a given function f : Expr → MetaM (Option α), and return the array of recognised values.

                                                                      Equations
                                                                        Instances For

                                                                          Check if an expression is an array literal (i.e. List.toArray applied to a nested chain of List.cons, ending at a List.nil), returning the array of Expr values.

                                                                          Equations
                                                                            Instances For