Documentation

Lean.Data.Parsec

Instances For
    instance Lean.Parsec.instReprParseResult :
    {α : Type} → [inst : Repr α] → Repr (Lean.Parsec.ParseResult α)
    Equations
    • Lean.Parsec.instReprParseResult = { reprPrec := Lean.Parsec.reprParseResult✝ }
    def Lean.Parsec (α : Type) :
    Equations
    Instances For
      @[inline]
      def Lean.Parsec.pure {α : Type} (a : α) :
      Equations
      Instances For
        @[inline]
        def Lean.Parsec.bind {α : Type} {β : Type} (f : Lean.Parsec α) (g : αLean.Parsec β) :
        Equations
        Instances For
          @[inline]
          def Lean.Parsec.fail {α : Type} (msg : String) :
          Equations
          Instances For
            @[inline]
            def Lean.Parsec.tryCatch {α : Type} {β : Type} (p : Lean.Parsec α) (csuccess : αLean.Parsec β) (cerror : UnitLean.Parsec β) :
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[inline]
              def Lean.Parsec.orElse {α : Type} (p : Lean.Parsec α) (q : UnitLean.Parsec α) :
              Equations
              • p.orElse q = p.tryCatch pure q
              Instances For
                @[inline]
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Lean.Parsec.run {α : Type} (p : Lean.Parsec α) (s : String) :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    Instances For
                      @[specialize #[]]
                      partial def Lean.Parsec.manyCore {α : Type} (p : Lean.Parsec α) (acc : Array α) :
                      @[inline]
                      Equations
                      • p.many = p.manyCore #[]
                      Instances For
                        @[inline]
                        Equations
                        • p.many1 = do let __do_liftp p.manyCore #[__do_lift]
                        Instances For
                          @[specialize #[]]
                          @[inline]
                          Equations
                          • p.manyChars = p.manyCharsCore ""
                          Instances For
                            @[inline]
                            Equations
                            • p.many1Chars = do let __do_liftp p.manyCharsCore __do_lift.toString
                            Instances For

                              Parses the given string.

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