Documentation

Lean.Meta.AppBuilder

Returns id e

Equations
    Instances For
      def Lean.Meta.mkExpectedTypeHintCore (e expectedType : Expr) (expectedTypeUniv : Level) :
      Equations
        Instances For
          def Lean.Meta.mkExpectedPropHint (proof expectedProp : Expr) :

          Given proof s.t. inferType proof is definitionally equal to expectedProp, returns term @id expectedProp proof.

          Equations
            Instances For

              Given e s.t. inferType e is definitionally equal to expectedType, returns term @id expectedType e.

              Equations
                Instances For

                  mkLetFun x v e creates the encoding for the let_fun x := v; e expression. The expression x can either be a free variable or a metavariable, and the function suitably abstracts x in e.

                  Equations
                    Instances For

                      Returns a = b.

                      Equations
                        Instances For

                          Returns HEq a b.

                          Equations
                            Instances For

                              If a and b have definitionally equal types, returns Eq a b, otherwise returns HEq a b.

                              Equations
                                Instances For

                                  Returns a proof of a = a.

                                  Equations
                                    Instances For

                                      Returns a proof of HEq a a.

                                      Equations
                                        Instances For
                                          def Lean.Meta.mkAbsurd (e hp hnp : Expr) :

                                          Given hp : P and nhp : Not P, returns an instance of type e.

                                          Equations
                                            Instances For

                                              Given h : False, returns an instance of type e.

                                              Equations
                                                Instances For

                                                  Given h : a = b, returns a proof of b = a.

                                                  Equations
                                                    Instances For
                                                      def Lean.Meta.mkEqTrans (h₁ h₂ : Expr) :

                                                      Given h₁ : a = b and h₂ : b = c, returns a proof of a = c.

                                                      Equations
                                                        Instances For

                                                          Similar to mkEqTrans, but arguments can be none. none is treated as a reflexivity proof.

                                                          Equations
                                                            Instances For

                                                              Given h : HEq a b, returns a proof of HEq b a.

                                                              Equations
                                                                Instances For
                                                                  def Lean.Meta.mkHEqTrans (h₁ h₂ : Expr) :

                                                                  Given h₁ : HEq a b, h₂ : HEq b c, returns a proof of HEq a c.

                                                                  Equations
                                                                    Instances For
                                                                      def Lean.Meta.mkEqOfHEq (h : Expr) (check : Bool := true) :

                                                                      Given h : HEq a b where a and b have the same type, returns a proof of Eq a b.

                                                                      Equations
                                                                        Instances For

                                                                          Given h : Eq a b, returns a proof of HEq a b.

                                                                          Equations
                                                                            Instances For

                                                                              If e is @Eq.refl α a, returns a.

                                                                              Equations
                                                                                Instances For

                                                                                  If e is @congrArg α β a b f h, returns α, f and h. Also works if e can be turned into such an application (e.g. congrFun).

                                                                                  Equations
                                                                                    Instances For
                                                                                      partial def Lean.Meta.mkCongrArg (f h : Expr) :

                                                                                      Given f : α → β and h : a = b, returns a proof of f a = f b.

                                                                                      Given h : f = g and a : α, returns a proof of f a = g a.

                                                                                      Equations
                                                                                        Instances For
                                                                                          def Lean.Meta.mkCongr (h₁ h₂ : Expr) :

                                                                                          Given h₁ : f = g and h₂ : a = b, returns a proof of f a = g b.

                                                                                          Equations
                                                                                            Instances For
                                                                                              def Lean.Meta.mkAppM (constName : Name) (xs : Array Expr) :

                                                                                              Returns the application constName xs. It tries to fill the implicit arguments before the last element in xs.

                                                                                              Remark: mkAppM `arbitrary #[α] returns @arbitrary.{u} α without synthesizing the implicit argument occurring after α. Given a x : ([Decidable p] → Bool) × Nat, mkAppM `Prod.fst #[x], returns @Prod.fst ([Decidable p] → Bool) Nat x.

                                                                                              Equations
                                                                                                Instances For

                                                                                                  Similar to mkAppM, but takes an Expr instead of a constant name.

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      def Lean.Meta.mkAppOptM (constName : Name) (xs : Array (Option Expr)) :

                                                                                                      Similar to mkAppM, but it allows us to specify which arguments are provided explicitly using Option type. Example: Given Pure.pure {m : Type u → Type v} [Pure m] {α : Type u} (a : α) : m α,

                                                                                                      mkAppOptM `Pure.pure #[m, none, none, a]
                                                                                                      

                                                                                                      returns a Pure.pure application if the instance Pure m can be synthesized, and the universe match. Note that,

                                                                                                      mkAppM `Pure.pure #[a]
                                                                                                      

                                                                                                      fails because the only explicit argument (a : α) is not sufficient for inferring the remaining arguments, we would need the expected type.

                                                                                                      Equations
                                                                                                        Instances For

                                                                                                          Similar to mkAppOptM, but takes an Expr instead of a constant name.

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              def Lean.Meta.mkEqNDRec (motive h1 h2 : Expr) :
                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  def Lean.Meta.mkEqRec (motive h1 h2 : Expr) :
                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      def Lean.Meta.mkEqMP (eqProof pr : Expr) :
                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          def Lean.Meta.mkEqMPR (eqProof pr : Expr) :
                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  def Lean.Meta.mkPure (monad e : Expr) :

                                                                                                                                  Given a monad and e : α, makes pure e.

                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      partial def Lean.Meta.mkProjection (s : Expr) (fieldName : Name) :

                                                                                                                                      mkProjection s fieldName returns an expression for accessing field fieldName of the structure s. Remark: fieldName may be a subfield of s.

                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  def Lean.Meta.mkSome (type value : Expr) :
                                                                                                                                                  Equations
                                                                                                                                                    Instances For

                                                                                                                                                      Returns Decidable.decide p

                                                                                                                                                      Equations
                                                                                                                                                        Instances For

                                                                                                                                                          Returns a proof for p : Prop using decide p

                                                                                                                                                          Equations
                                                                                                                                                            Instances For

                                                                                                                                                              Returns a < b

                                                                                                                                                              Equations
                                                                                                                                                                Instances For

                                                                                                                                                                  Returns a <= b

                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For

                                                                                                                                                                      Returns Inhabited.default α

                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For

                                                                                                                                                                          Returns @Classical.ofNonempty α _

                                                                                                                                                                          Equations
                                                                                                                                                                            Instances For

                                                                                                                                                                              Returns funext h

                                                                                                                                                                              Equations
                                                                                                                                                                                Instances For

                                                                                                                                                                                  Returns propext h

                                                                                                                                                                                  Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      def Lean.Meta.mkLetCongr (h₁ h₂ : Expr) :

                                                                                                                                                                                      Returns let_congr h₁ h₂

                                                                                                                                                                                      Equations
                                                                                                                                                                                        Instances For

                                                                                                                                                                                          Returns let_val_congr b h

                                                                                                                                                                                          Equations
                                                                                                                                                                                            Instances For

                                                                                                                                                                                              Returns let_body_congr a h

                                                                                                                                                                                              Equations
                                                                                                                                                                                                Instances For

                                                                                                                                                                                                  Returns @of_eq_false p h

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                      Returns of_eq_false h

                                                                                                                                                                                                      Equations
                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                          Returns @of_eq_true p h

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                              Returns of_eq_true h

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                  Returns eq_true h

                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                      Returns eq_true h

                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                          Returns eq_false h h must have type definitionally equal to ¬ p in the current reducibility setting.

                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                              Returns eq_false' h h must have type definitionally equal to p → False in the current reducibility setting.

                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  def Lean.Meta.mkImpCongr (h₁ h₂ : Expr) :
                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                  Returns instance for [Monad m] if there is one

                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                      def Lean.Meta.mkNumeral (type : Expr) (n : Nat) :

                                                                                                                                                                                                                                                      Returns (n : type), a numeric literal of type type. The method fails if we don't have an instance OfNat type n

                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                          Returns a + b using a heterogeneous +. This method assumes a and b have the same type.

                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                              Returns a - b using a heterogeneous -. This method assumes a and b have the same type.

                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                  Returns a * b using a heterogeneous *. This method assumes a and b have the same type.

                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                      Returns a ≤ b. This method assumes a and b have the same type.

                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                          Returns a < b. This method assumes a and b have the same type.

                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                              Given h : a = b, returns a proof for a ↔ b.

                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                Instances For