Documentation

Lean.Elab.Command

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

                          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.

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