Documentation

Lean.Elab.PreDefinition.Eqns

Instances For
    partial def Lean.Elab.Eqns.expand (progress : Bool) (e : Expr) :

    Zeta reduces let and let_fun while consuming metadata. Returns true if progress is made.

    Equations
      Instances For
        Equations
          Instances For
            Equations
              Instances For
                Equations
                  Instances For
                    partial def Lean.Elab.Eqns.splitMatch?.go (mvarId : MVarId) (declNames : Array Name) (target : Expr) (badCases : ExprSet) :

                    Try to close goal using rfl with smart unfolding turned off.

                    Equations
                      Instances For

                        Eliminate namedPatterns from equation, and trivial hypotheses.

                        Equations
                          Instances For
                            def Lean.Elab.Eqns.mkEqnTypes (declNames : Array Name) (mvarId : MVarId) :
                            Equations
                              Instances For

                                Some of the hypotheses added by mkEqnTypes may not be used by the actual proof (i.e., value argument). This method eliminates them.

                                Alternative solution: improve saveEqn and make sure it never includes unnecessary hypotheses. These hypotheses are leftovers from tactics such as splitMatch? used in mkEqnTypes.

                                Equations
                                  Instances For
                                    def Lean.Elab.Eqns.removeUnusedEqnHypotheses.go (declType declValue type value : Expr) (xs : Array Expr) (lctx : LocalContext) :
                                    Equations
                                      Instances For

                                        Delta reduce the equation left-hand-side

                                        Equations
                                          Instances For
                                            def Lean.Elab.Eqns.deltaRHS? (mvarId : MVarId) (declName : Name) :
                                            Equations
                                              Instances For

                                                Apply whnfR to lhs, return none if lhs was not modified

                                                Equations
                                                  Instances For
                                                    Equations
                                                      Instances For
                                                        def Lean.Elab.Eqns.mkEqns (declName : Name) (declNames : Array Name) (tryRefl : Bool := true) :

                                                        Generate equations for declName.

                                                        This unfolds the function application on the LHS (using an unfold theorem, if present, or else by delta-reduction), calculates the types for the equational theorems using mkEqnTypes, and then proves them using mkEqnProof.

                                                        This is currently used for non-recursive functions, well-founded recursion and partial_fixpoint, but not for structural recursion.

                                                        Equations
                                                          Instances For
                                                            def Lean.Elab.Eqns.mkEqns.doRealize (declName : Name) (tryRefl : Bool := true) (name : Name) (info : DefinitionVal) (type : Expr) :
                                                            Equations
                                                              Instances For
                                                                def Lean.Elab.Eqns.mkUnfoldProof (declName : Name) (mvarId : MVarId) :

                                                                Auxiliary method for mkUnfoldEq. The structure is based on mkEqnTypes. mvarId is the goal to be proved. It is a goal of the form

                                                                declName x_1 ... x_n = body[x_1, ..., x_n]
                                                                

                                                                The proof is constructed using the automatically generated equational theorems. We basically keep splitting the match and if-then-else expressions in the right hand side until one of the equational theorems is applicable.

                                                                Equations
                                                                  Instances For
                                                                    partial def Lean.Elab.Eqns.mkUnfoldProof.go (declName : Name) (tryEqns : MVarIdMetaM Bool) (mvarId : MVarId) :