Documentation

Lean.Elab.Command

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

        Like Core.tryCatchRuntimeEx; runtime errors are generally used to abort term elaboration, so we do want to catch and process them at the command level.

        Equations
        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.
            Equations
            • One or more equations did not get rendered due to their size.
            @[always_inline]
            Equations
            Equations
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[inline]
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      Instances For
                        Equations
                        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.
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[implemented_by Lean.Elab.Command.mkCommandElabAttributeUnsafe]

                              Disables incremental command reuse and reporting for act if cond is true by setting Context.snap? to none.

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

                                Elaborate x with stx on the macro stack

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

                                  Snapshot after macro expansion of a command.

                                  Instances For

                                    Option for showing elaboration errors from partial syntax errors.

                                    elabCommand wrapper that should be used for the initial invocation, not for recursive calls after macro expansion etc.

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

                                      Adapt a syntax transformation to a regular, command-producing elaborator.

                                      Equations
                                      Instances For
                                        Equations
                                        • Lean.Elab.Command.instInhabitedCommandElabM = { default := throw default }

                                        Return identifier names in the given bracketed binder.

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

                                          Lift the TermElabM monadic action x into a CommandElabM monadic action.

                                          Note that x is executed with an empty message log. Thus, x cannot modify/view messages produced by previous commands.

                                          If you need to access the free variables corresponding to the ones declared using the variable command, consider using runTermElabM.

                                          Recall that TermElabM actions can automatically lift MetaM and CoreM actions. Example:

                                          import Lean
                                          
                                          open Lean Elab Command Meta
                                          
                                          def printExpr (e : Expr) : MetaM Unit := do
                                            IO.println s!"{← ppExpr e} : {← ppExpr (← inferType e)}"
                                          
                                          #eval
                                            liftTermElabM do
                                              printExpr (mkConst ``Nat)
                                          
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            Execute the monadic action elabFn xs as a CommandElabM monadic action, where xs are free variables corresponding to all active scoped variables declared using the variable command.

                                            This method is similar to liftTermElabM, but it elaborates all scoped variables declared using the variable command.

                                            Example:

                                            import Lean
                                            
                                            open Lean Elab Command Meta
                                            
                                            variable {α : Type u} {f : α → α}
                                            variable (n : Nat)
                                            
                                            #eval
                                              runTermElabM fun xs => do
                                                for x in xs do
                                                  IO.println s!"{← ppExpr x} : {← ppExpr (← inferType x)}"
                                            
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[inline]

                                              Catches and logs exceptions occurring in x. Unlike try catch in CommandElabM, this function catches interrupt exceptions as well and thus is intended for use at the top level of elaboration. Interrupt and abort exceptions are caught but not logged.

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

                                                        Lifts an action in CommandElabM into CoreM, updating the traces and the environment.

                                                        Commands that modify the processing of subsequent commands, such as open and namespace commands, only have an effect for the remainder of the CommandElabM computation passed here, and do not affect subsequent commands.

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

                                                          Given a command elaborator cmd, returns a new command elaborator that first evaluates any local set_option ... in ... clauses and then invokes cmd on what remains.