Documentation

Lean.Meta.AppBuilder

Return id e

Equations
Instances For

    Given e s.t. inferType e is definitionally equal to expectedType, return 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
      • One or more equations did not get rendered due to their size.
      Instances For

        Return a = b.

        Equations
        Instances For

          Return HEq a b.

          Equations
          Instances For

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Return a proof of a = a.

              Equations
              Instances For

                Return a proof of HEq a a.

                Equations
                Instances For

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

                  Equations
                  Instances For

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

                    Equations
                    Instances For

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

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

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

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

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

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

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

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

                                  Equations
                                  Instances For

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

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      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
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

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

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          Return 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
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

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

                                            Equations
                                            Instances For

                                              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
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

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

                                                Equations
                                                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
                                                      Equations
                                                      Instances For
                                                        Equations
                                                        Instances For
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For

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

                                                            Equations
                                                            Instances For

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

                                                              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

                                                                        Return Decidable.decide p

                                                                        Equations
                                                                        Instances For

                                                                          Return a proof for p : Prop using decide p

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For

                                                                            Return a < b

                                                                            Equations
                                                                            Instances For

                                                                              Return a <= b

                                                                              Equations
                                                                              Instances For

                                                                                Return Inhabited.default α

                                                                                Equations
                                                                                Instances For

                                                                                  Return @Classical.ofNonempty α _

                                                                                  Equations
                                                                                  Instances For

                                                                                    Return sorryAx type

                                                                                    Equations
                                                                                    Instances For

                                                                                      Return funext h

                                                                                      Equations
                                                                                      Instances For

                                                                                        Return let_congr h₁ h₂

                                                                                        Equations
                                                                                        Instances For

                                                                                          Return let_val_congr b h

                                                                                          Equations
                                                                                          Instances For

                                                                                            Return let_body_congr a h

                                                                                            Equations
                                                                                            Instances For

                                                                                              Return eq_true h

                                                                                              Equations
                                                                                              Instances For

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

                                                                                                Equations
                                                                                                Instances For

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

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        Equations
                                                                                                        Instances For

                                                                                                          Return instance for [Monad m] if there is one

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For

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

                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For

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

                                                                                                              Equations
                                                                                                              Instances For

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

                                                                                                                Equations
                                                                                                                Instances For

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

                                                                                                                  Equations
                                                                                                                  Instances For

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

                                                                                                                    Equations
                                                                                                                    Instances For

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

                                                                                                                      Equations
                                                                                                                      Instances For

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

                                                                                                                        Equations
                                                                                                                        Instances For