Documentation

Lean.Elab.Command

Instances For
    Instances For
      Instances For
        @[inline, reducible]
        Instances For
          @[inline, reducible]
          Instances For
            @[inline, reducible]
            Instances For
              @[inline]
              Instances For
                @[implemented_by Lean.Elab.Command.mkCommandElabAttributeUnsafe]

                Elaborate x with stx on the macro stack

                Instances For

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

                  Instances For

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

                    Instances For

                      Return identifier names in the given bracketed binder.

                      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)
                        
                        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)}"
                          
                          Instances For