Documentation

Lean.Data.Parsec

@[inline]
def Lean.Parsec.pure {α : Type} (a : α) :
Instances For
    @[inline]
    def Lean.Parsec.bind {α : Type} {β : Type} (f : Lean.Parsec α) (g : αLean.Parsec β) :
    Instances For
      @[inline]
      def Lean.Parsec.fail {α : Type} (msg : String) :
      Instances For
        @[inline]
        def Lean.Parsec.orElse {α : Type} (p : Lean.Parsec α) (q : UnitLean.Parsec α) :
        Instances For
          @[inline]
          Instances For
            def Lean.Parsec.run {α : Type} (p : Lean.Parsec α) (s : String) :
            Instances For
              @[inline]
              Instances For
                @[specialize #[]]
                partial def Lean.Parsec.manyCore {α : Type} (p : Lean.Parsec α) (acc : Array α) :
                @[inline]
                Instances For
                  @[inline]
                  Instances For
                    @[specialize #[]]

                    Parses the given string.

                    Instances For
                      @[inline]
                      Instances For
                        @[inline]
                        Instances For
                          @[inline]
                          Instances For
                            @[inline]
                            Instances For
                              @[inline]
                              Instances For
                                @[inline]
                                Instances For
                                  @[inline]
                                  Instances For
                                    @[inline]
                                    Instances For
                                      @[inline]
                                      Instances For
                                        @[inline]
                                        Instances For
                                          @[inline]
                                          Instances For
                                            @[inline]
                                            Instances For
                                              @[inline]
                                              Instances For