Documentation

Batteries.Lean.Meta.Basic

Sort the given FVarIds by the order in which they appear in the current local context. If any of the FVarIds do not appear in the current local context, the result is unspecified.

Equations
Instances For

    Get the MetavarDecl of mvarId. If mvarId is not a declared metavariable in the given MetavarContext, throw an error.

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

      Declare a metavariable. You must make sure that the metavariable is not already declared.

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

        Check whether a metavariable is assigned or delayed-assigned. A delayed-assigned metavariable is already 'solved' but the solution cannot be substituted yet because we have to wait for some other metavariables to be assigned first. So in most situations you want to treat a delayed-assigned metavariable as assigned.

        Equations
        • mctx.isExprMVarAssignedOrDelayedAssigned mvarId = (mctx.eAssignment.contains mvarId || mctx.dAssignment.contains mvarId)
        Instances For

          Check whether a metavariable is declared in the given MetavarContext.

          Equations
          • mctx.isExprMVarDeclared mvarId = mctx.decls.contains mvarId
          Instances For

            Erase any assignment or delayed assignment of the given metavariable.

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

              Obtain all unassigned metavariables from the given MetavarContext. If includeDelayed is true, delayed-assigned metavariables are considered unassigned.

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

                Check whether a metavariable is declared.

                Equations
                • mvarId.isDeclared = do let __do_liftLean.getMCtx pure (__do_lift.isExprMVarDeclared mvarId)
                Instances For

                  Erase any assignment or delayed assignment of the given metavariable.

                  Equations
                  Instances For

                    Solve a goal by synthesizing an instance.

                    Equations
                    Instances For

                      Get the type the given metavariable after instantiating metavariables and cleaning up annotations.

                      Equations
                      • mvarId.getTypeCleanup = do let __do_liftmvarId.getType let __do_liftLean.instantiateMVars __do_lift pure __do_lift.cleanupAnnotations
                      Instances For

                        Obtain all unassigned metavariables. If includeDelayed is true, delayed-assigned metavariables are considered unassigned.

                        Equations
                        Instances For
                          def Lean.Meta.unhygienic {m : TypeType} {α : Type} [Lean.MonadWithOptions m] (x : m α) :
                          m α

                          Run a computation with hygiene turned off.

                          Equations
                          Instances For

                            A variant of mkFreshId which generates names with a particular prefix. The generated names are unique and have the form <prefix>.<N> where N is a natural number. They are not suitable as user-facing names.

                            Equations
                            Instances For

                              saturate1 goal tac runs tac on goal, then on the resulting goals, etc., until tac does not apply to any goal any more (i.e. it returns none). The order of applications is depth-first, so if tac generates goals [g₁, g₂, ⋯], we apply tac to g₁ and recursively to all its subgoals before visiting g₂. If tac does not apply to goal, saturate1 returns none. Otherwise it returns the generated subgoals to which tac did not apply. saturate1 respects the MonadRecDepth recursion limit.

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

                                Auxiliary definition for saturate1.