Documentation

Lean.Elab.App

Equations
    Instances For
      Equations
        Instances For
          Equations
            Instances For
              def Lean.Elab.Term.eraseNamedArg (namedArgs : List NamedArg) (binderName : Name) :

              Erase entry for binderName from namedArgs.

              Equations
                Instances For

                  Default application elaborator #

                  • ellipsis : Bool

                    true if .. was used

                  • explicit : Bool

                    true if @ modifier was used

                  • resultIsOutParamSupport : Bool

                    If the result type of an application is the outParam of some local instance, then special support may be needed because type class resolution interacts poorly with coercions in this kind of situation. This flag enables the special support.

                    The idea is quite simple, if the result type is the outParam of some local instance, we simply execute synthesizeSyntheticMVarsUsingDefault. We added this feature to make sure examples as follows are correctly elaborated.

                    class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
                      getElem (xs : Cont) (i : Idx) : Elem
                    
                    export GetElem (getElem)
                    
                    instance : GetElem (Array α) Nat α where
                      getElem xs i := xs.get ⟨i, sorry⟩
                    
                    opaque f : Option BoolBool
                    opaque g : BoolBool
                    
                    def bad (xs : Array Bool) : Bool :=
                      let x := getElem xs 0
                      f x && g x
                    

                    Without the special support, Lean fails at g x saying x has type Option Bool but is expected to have type Bool. From the user's point of view this is a bug, since let x := getElem xs 0 clearly constrains x to be Bool, but we only obtain this information after we apply the OfNat default instance for 0.

                    Before converging to this solution, we have tried to create a "coercion placeholder" when resultIsOutParamSupport = true, but it did not work well in practice. For example, it failed in the example above.

                  Instances For

                    Auxiliary structure for elaborating the application f args namedArgs.

                    • f : Expr
                    • fType : Expr
                    • args : List Arg

                      Remaining regular arguments.

                    • namedArgs : List NamedArg

                      remaining named arguments to be processed.

                    • expectedType? : Option Expr
                    • etaArgs : Array Expr

                      When named arguments are provided and explicit arguments occurring before them are missing, the elaborator eta-expands the declaration. For example,

                      def f (x y : Nat) := x + y
                      #check f (y := 5)
                      -- fun x => f x 5
                      

                      etaArgs stores the fresh free variables for implementing the eta-expansion. When .. is used, eta-expansion is disabled, and missing arguments are treated as _.

                    • toSetErrorCtx : Array MVarId

                      Metavariables that we need to set the error context using the application being built.

                    • instMVars : Array MVarId

                      Metavariables for the instance implicit arguments that have already been processed.

                    • propagateExpected : Bool

                      The following field is used to implement the propagateExpectedType heuristic. It is set to true true when expectedType still has to be propagated.

                    • resultTypeOutParam? : Option MVarId

                      If the result type may be the outParam of some local instance. See comment at Context.resultIsOutParamSupport

                    Instances For
                      @[reducible, inline]
                      Equations
                        Instances For

                          Try to synthesize metavariables are instMVars using type class resolution. The ones that cannot be synthesized yet stay in the instMVars list. Remark: we use this method

                          • before trying to apply coercions to function,
                          • before unifying the expected type.
                          Equations
                            Instances For

                              Try to synthesize metavariables are instMVars using type class resolution. The ones that cannot be synthesized yet are registered.

                              Equations
                                Instances For

                                  Remove named argument with name binderName from namedArgs.

                                  Equations
                                    Instances For

                                      Elaborate function application arguments.

                                      Eliminator-like function application elaborator #

                                      Information about an eliminator used by the elab-as-elim elaborator. This is not to be confused with Lean.Meta.ElimInfo, which is for induction and cases. The elab-as-elim routine is less restrictive in what counts as an eliminator, and it doesn't need to have a strict notion of what is a "target" — all it cares about are

                                      1. that the return type of a function is of the form m ... where m is a parameter (unlike induction and cases eliminators, the arguments to m, known as "discriminants", can be any expressions, not just parameters), and
                                      2. which arguments should be eagerly elaborated, to make discriminants be as elaborated as possible for the expected type generalization procedure, and which should be postponed (since they are the "minor premises").

                                      Note that the routine isn't doing induction/cases on particular expressions. The purpose of elab-as-elim is to successfully solve the higher-order unification problem between the return type of the function and the expected type.

                                      • elimExpr : Expr

                                        The eliminator.

                                      • elimType : Expr

                                        The type of the eliminator.

                                      • motivePos : Nat

                                        The position of the motive parameter.

                                      • majorsPos : Array Nat

                                        Positions of "major" parameters (those that should be eagerly elaborated because they can contribute to the motive inference procedure). All parameters that are neither the motive nor a major parameter are "minor" parameters. The major parameters include all of the parameters that transitively appear in the motive's arguments, as well as "first-order" arguments that include such parameters, since they too can help with elaborating discriminants.

                                        For example, in the following theorem the argument h : a = b should be elaborated eagerly because it contains b, which occurs in motive b.

                                        theorem Eq.subst' {α} {motive : α → Prop} {a b : α} (h : a = b) : motive a → motive b
                                        

                                        For another example, the term isEmptyElim (α := α) is an underapplied eliminator, and it needs argument α to be elaborated eagerly to create a type-correct motive.

                                        def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := ...
                                        example {α : Type _} [IsEmpty α] : id (α → False) := isEmptyElim (α := α)
                                        
                                      Instances For
                                        Equations
                                          Instances For
                                            Equations
                                              Instances For

                                                Context of the elab_as_elim elaboration procedure.

                                                Instances For

                                                  State of the elab_as_elim elaboration procedure.

                                                  • f : Expr

                                                    The resultant expression being built.

                                                  • fType : Expr

                                                    `f : fType

                                                  • namedArgs : List NamedArg

                                                    User-provided named arguments that still have to be processed.

                                                  • args : List Arg

                                                    User-provided arguments that still have to be processed.

                                                  • instMVars : Array MVarId

                                                    Instance implicit arguments collected so far.

                                                  • idx : Nat

                                                    Position of the next argument to be processed. We use it to decide whether the argument is the motive or a discriminant.

                                                  • motive? : Option Expr

                                                    Store the metavariable used to represent the motive that will be computed at finalize.

                                                  Instances For
                                                    @[reducible, inline]
                                                    Equations
                                                      Instances For
                                                        def Lean.Elab.Term.ElabElim.mkMotive (discrs : Array Expr) (expectedType : Expr) :

                                                        Infer the motive using the expected type by kabstracting the discriminants.

                                                        Equations
                                                          Instances For

                                                            If the eliminator is over-applied, we "revert" the extra arguments. Returns the function with the reverted arguments applied and the new generalized expected type.

                                                            Equations
                                                              Instances For

                                                                Construct the resulting application after all discriminants have been elaborated, and we have consumed as many given arguments as possible.

                                                                Equations
                                                                  Instances For
                                                                    def Lean.Elab.Term.ElabElim.getNextArg? (binderName : Name) (binderInfo : BinderInfo) :

                                                                    Return the next argument to be processed. The result is .none if it is an implicit argument which was not provided using a named argument. The result is .undef if args is empty and namedArgs does contain an entry for binderName.

                                                                    Equations
                                                                      Instances For

                                                                        Set the motive field in the state.

                                                                        Equations
                                                                          Instances For
                                                                            def Lean.Elab.Term.ElabElim.saveArgInfo (arg : Expr) (binderName : Name) :

                                                                            Save information for producing error messages.

                                                                            Equations
                                                                              Instances For

                                                                                Create an implicit argument using the given BinderInfo.

                                                                                Equations
                                                                                  Instances For

                                                                                    Main loop of the elimAsElab procedure.

                                                                                    Function application elaboration #

                                                                                    def Lean.Elab.Term.elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis : Bool) (resultIsOutParamSupport : Bool := true) :

                                                                                    Elaborate a f-application using namedArgs and args as the arguments.

                                                                                    • expectedType? the expected type if available. It is used to propagate typing information only. This method does not ensure the result has this type.
                                                                                    • explicit = true when notation @ is used, and implicit arguments are assumed to be provided at namedArgs and args.
                                                                                    • ellipsis = true when notation .. is used. That is, we add _ for missing arguments.
                                                                                    • resultIsOutParamSupport is used to control whether special support is used when processing applications of functions that return output parameter of some local instance. Example:
                                                                                      GetElem.getElem : {Cont : Type u_1} → {Idx : Type u_2} → {elem : Type u_3} → {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] → (xs : cont) → (i : idx) → dom xs i → elem
                                                                                      
                                                                                      The result type elem is the output parameter of the local instance self. When this parameter is set to true, we execute synthesizeSyntheticMVarsUsingDefault. For additional details, see comment at ElabAppArgs.resultIsOutParam.
                                                                                    Equations
                                                                                      Instances For
                                                                                        def Lean.Elab.Term.elabAppArgs.elabAsElim? (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg) (explicit ellipsis : Bool) :

                                                                                        Return some info if we should elaborate as an eliminator.

                                                                                        Equations
                                                                                          Instances For

                                                                                            Auxiliary inductive datatype that represents the resolution of an LVal.

                                                                                            • projFn (baseStructName structName fieldName : Name) : LValResolution

                                                                                              When applied to f, effectively expands to BaseStruct.fieldName (self := Struct.toBase f). This is a special named argument where it suppresses any explicit arguments depending on it so that type parameters don't need to be supplied.

                                                                                            • projIdx (structName : Name) (idx : Nat) : LValResolution

                                                                                              Similar to projFn, but for extracting field indexed by idx. Works for structure-like inductive types in general.

                                                                                            • const (baseStructName structName constName : Name) : LValResolution

                                                                                              When applied to f, effectively expands to constName ... (Struct.toBase f), with the argument placed in the correct positional argument if possible, or otherwise as a named argument. The Struct.toBase is not present if baseStructName == structName, in which case these do not need to be structures. Supports generalized field notation.

                                                                                            • localRec (baseName fullName : Name) (fvar : Expr) : LValResolution

                                                                                              Like const, but with fvar instead of constName. The fullName is the name of the recursive function, and baseName is the base name of the type to search for in the parameter list.

                                                                                            Instances For

                                                                                              Interaction between errToSorry and observing. #

                                                                                              observing x does not check for synthetic sorry's, just an exception. Thus, it may think x worked when it didn't if a synthetic sorry was introduced. We decided that checking for synthetic sorrys at observing is not a good solution because it would not be clear to decide what the "main" error message for the alternative is. When the result contains a synthetic sorry, it is not clear which error message corresponds to the sorry. Moreover, while executing x, many error messages may have been logged. Recall that we need an error per alternative at mergeFailures.

                                                                                              Thus, we decided to set errToSorry to false whenever processing choice nodes and overloaded symbols.

                                                                                              Important: we rely on the property that after errToSorry is set to false, no elaboration function executed by x will reset it to true.

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