Documentation

Std.Internal.Parsec.Basic

Instances For
    Equations
    Instances For
      class Std.Internal.Parsec.Input (ι : Type) (elem idx : outParam Type) [DecidableEq idx] [DecidableEq elem] :
      • pos : ιidx
      • next : ιι
      • curr : ιelem
      • hasNext : ιBool
      • next' (it : ι) : hasNext it = trueι
      • curr' (it : ι) : hasNext it = trueelem
      Instances
        @[inline]
        def Std.Internal.Parsec.pure {α ι : Type} (a : α) :
        Parsec ι α
        Equations
        Instances For
          @[inline]
          def Std.Internal.Parsec.bind {ι α β : Type} (f : Parsec ι α) (g : αParsec ι β) :
          Parsec ι β
          Equations
          Instances For
            @[inline]
            def Std.Internal.Parsec.fail {α ι : Type} (msg : String) :
            Parsec ι α
            Equations
            Instances For
              @[inline]
              def Std.Internal.Parsec.tryCatch {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] {β : Type} (p : Parsec ι α) (csuccess : αParsec ι β) (cerror : UnitParsec ι β) :
              Parsec ι β
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[inline]
                def Std.Internal.Parsec.orElse {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι α) (q : UnitParsec ι α) :
                Parsec ι α
                Equations
                • p.orElse q = p.tryCatch pure q
                Instances For
                  @[inline]
                  def Std.Internal.Parsec.attempt {α ι : Type} (p : Parsec ι α) :
                  Parsec ι α
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[inline]
                    def Std.Internal.Parsec.eof {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[specialize #[]]
                      partial def Std.Internal.Parsec.manyCore {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι α) (acc : Array α) :
                      Parsec ι (Array α)
                      @[inline]
                      def Std.Internal.Parsec.many {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι α) :
                      Parsec ι (Array α)
                      Equations
                      • p.many = p.manyCore #[]
                      Instances For
                        @[inline]
                        def Std.Internal.Parsec.many1 {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι α) :
                        Parsec ι (Array α)
                        Equations
                        • p.many1 = do let __do_liftp p.manyCore #[__do_lift]
                        Instances For
                          @[inline]
                          def Std.Internal.Parsec.any {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] :
                          Parsec ι elem
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[inline]
                            def Std.Internal.Parsec.satisfy {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : elemBool) :
                            Parsec ι elem
                            Equations
                            Instances For
                              @[inline]
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[inline]
                                def Std.Internal.Parsec.peek? {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] :
                                Parsec ι (Option elem)
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[inline]
                                  def Std.Internal.Parsec.peek! {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] :
                                  Parsec ι elem
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[inline]
                                    def Std.Internal.Parsec.peekD {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (default : elem) :
                                    Parsec ι elem
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[inline]
                                      def Std.Internal.Parsec.skip {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] :
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[specialize #[]]
                                        partial def Std.Internal.Parsec.manyCharsCore {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι Char) (acc : String) :
                                        @[inline]
                                        def Std.Internal.Parsec.manyChars {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι Char) :
                                        Equations
                                        • p.manyChars = p.manyCharsCore ""
                                        Instances For
                                          @[inline]
                                          def Std.Internal.Parsec.many1Chars {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Input ι elem idx] (p : Parsec ι Char) :
                                          Equations
                                          • p.many1Chars = do let __do_liftp p.manyCharsCore __do_lift.toString
                                          Instances For