Documentation

Lean.Elab.PreDefinition.Eqns

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

              Eliminate namedPatterns from equation, and trivial hypotheses.

              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
                  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
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def Lean.Elab.Eqns.removeUnusedEqnHypotheses.go (declType declValue type value : Expr) (xs : Array Expr) (lctx : LocalContext) :
                      Instances For

                        Delta reduce the equation left-hand-side

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def Lean.Elab.Eqns.deltaRHS? (mvarId : MVarId) (declName : Name) :
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

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

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

                                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 and for functions defined by partial_fixpoint.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                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
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    partial def Lean.Elab.Eqns.mkUnfoldProof.go (declName : Name) (tryEqns : MVarIdMetaM Bool) (mvarId : MVarId) :

                                    Generate the "unfold" lemma for declName.

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