Documentation

Std.Lean.Meta.Basic

Set the kind of a LocalDecl.

Instances For

    Set the kind of the given fvar.

    Instances For

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

      Instances For

        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.

        Instances For

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

          Instances For

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

            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.

              Instances For

                Check whether a metavariable is declared in the given MetavarContext.

                Instances For

                  Add a delayed assignment for the given metavariable. You must make sure that the metavariable is not already assigned or delayed-assigned.

                  Instances For

                    Erase any assignment or delayed assignment of the given metavariable.

                    Instances For

                      Modify the declaration of a metavariable. If the metavariable is not declared, the MetavarContext is returned unchanged.

                      You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.

                      Instances For

                        Modify the local context of a metavariable. If the metavariable is not declared, the MetavarContext is returned unchanged.

                        You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.

                        Instances For

                          Set the kind of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, the MetavarContext is returned unchanged.

                          Instances For

                            Set the BinderInfo of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, the MetavarContext is returned unchanged.

                            Instances For

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

                              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.

                                Instances For

                                  Check whether a metavariable is declared.

                                  Instances For

                                    Add a delayed assignment for the given metavariable. You must make sure that the metavariable is not already assigned or delayed-assigned.

                                    Instances For

                                      Erase any assignment or delayed assignment of the given metavariable.

                                      Instances For

                                        Modify the declaration of a metavariable. If the metavariable is not declared, nothing happens.

                                        You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.

                                        Instances For

                                          Modify the local context of a metavariable. If the metavariable is not declared, nothing happens.

                                          You must ensure that the modification is legal. In particular, expressions may only be replaced with defeq expressions.

                                          Instances For

                                            Set the kind of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, nothing happens.

                                            Instances For

                                              Set the BinderInfo of an fvar. If the given metavariable is not declared or the given fvar doesn't exist in its context, nothing happens.

                                              Instances For

                                                Collect the metavariables which mvarId depends on. These are the metavariables which appear in the type and local context of mvarId, as well as the metavariables which those metavariables depend on, etc.

                                                Instances For

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

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

                                                    Run a computation with hygiene turned off.

                                                    Instances For

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

                                                      Instances For

                                                        Implementation of repeat' and repeat1'.

                                                        repeat'Core f runs f on all of the goals to produce a new list of goals, then runs f again on all of those goals, and repeats until f fails on all remaining goals, or until maxIters total calls to f have occurred.

                                                        Returns a boolean indicating whether f succeeded at least once, and all the remaining goals (i.e. those on which f failed).

                                                        Instances For

                                                          Auxiliary for repeat'Core. repeat'Core.go f maxIters progress gs stk acc evaluates to essentially acc.toList ++ repeat' f (gs::stk).join maxIters: that is, acc are goals we will not revisit, and (gs::stk).join is the accumulated todo list of subgoals.

                                                          Equations
                                                          Instances For
                                                            def Lean.Meta.repeat' {m : TypeType} [Monad m] [Lean.MonadError m] [Lean.MonadMCtx m] (f : Lean.MVarIdm (List Lean.MVarId)) (gs : List Lean.MVarId) (maxIters : optParam Nat 100000) :

                                                            repeat' f runs f on all of the goals to produce a new list of goals, then runs f again on all of those goals, and repeats until f fails on all remaining goals, or until maxIters total calls to f have occurred. Always succeeds (returning the original goals if f fails on all of them).

                                                            Instances For
                                                              def Lean.Meta.repeat1' {m : TypeType} [Monad m] [Lean.MonadError m] [Lean.MonadMCtx m] (f : Lean.MVarIdm (List Lean.MVarId)) (gs : List Lean.MVarId) (maxIters : optParam Nat 100000) :

                                                              repeat1' f runs f on all of the goals to produce a new list of goals, then runs f again on all of those goals, and repeats until f fails on all remaining goals, or until maxIters total calls to f have occurred. Fails if f does not succeed at least once.

                                                              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.

                                                                Instances For

                                                                  Auxiliary definition for saturate1.