Documentation

Aesop.Script

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    Equations
    Instances For
      @[inline]
      Equations
      Instances For
        @[inline]
        Equations
        Instances For
          @[inline]
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[inline]
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[inline]
              Equations
              • Aesop.UnstructuredScriptBuilder.id = pure #[]
              Instances For
                Equations
                • Aesop.UnstructuredScriptBuilder.instInhabitedUnstructuredScriptBuilder = { default := pure #[] }
                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
                      @[inline]
                      Equations
                      Instances For
                        Equations
                        • Aesop.StructuredScriptBuilder.instInhabitedStructuredScriptBuilder = { default := Aesop.StructuredScriptBuilder.id }
                        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
                            structure Aesop.ScriptBuilder (m : TypeType) :
                            Instances For
                              Equations
                              • Aesop.instInhabitedScriptBuilder = { default := { unstructured := default, structured := default } }
                              Equations
                              • Aesop.ScriptBuilder.id = { unstructured := Aesop.UnstructuredScriptBuilder.id, structured := Aesop.StructuredScriptBuilder.id }
                              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
                                        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
                                            @[always_inline]
                                            def Aesop.ScriptBuilder.withPrefix {m : TypeType} [Monad m] [Lean.MonadQuotation m] [Lean.MonadError m] (f : Lean.TSyntax `Lean.Parser.Tactic.tacticSeqm (Array (Lean.TSyntax `tactic))) (b : Aesop.ScriptBuilder m) :
                                            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
                                                  @[always_inline]
                                                  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
                                                            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
                                                                  Instances For
                                                                    Equations
                                                                    Equations
                                                                    Instances For
                                                                      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.
                                                                              Instances For
                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  @[always_inline]
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    Equations
                                                                                    Instances For
                                                                                      Equations
                                                                                      • Aesop.TacticInvocation.noop preGoal postGoal preState postState = { preState := preState, preGoal := preGoal, tacticSeq := #[], postGoals := #[postGoal], postState := postState }
                                                                                      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
                                                                                                Equations
                                                                                                Instances For
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For