Documentation

Lean.Elab.PreDefinition.Eqns

Instances For
    Equations
    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
            Instances For
              partial def Lean.Elab.Eqns.splitMatch?.go (mvarId : Lean.MVarId) (declNames : Array Lake.Name) (target : Lean.Expr) (badCases : Lean.ExprSet) :
              Instances For

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

                          Delta reduce the equation left-hand-side

                          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

                              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

                                  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 constracted 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

                                    Generate the "unfold" lemma for declName.

                                    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