Documentation

Regex.Syntax.Parser.Combinators.Result

source
inductive Regex.Syntax.Parser.Combinators.Result (s : Bool) (it : String.Iterator) (ε α : Type) :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Regex.Syntax.Parser.Combinators.Result.LE (it : String.Iterator) (ε α : Type) :
    Type
    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Regex.Syntax.Parser.Combinators.Result.LT (it : String.Iterator) (ε α : Type) :
      Type
      Equations
      Instances For
        source
        @[inline]
        def Regex.Syntax.Parser.Combinators.Result.imp {s₁ s₂ : Bool} {it : String.Iterator} {ε α : Type} (h : s₂ = true → s₁ = true) :
        Result s₁ it ε α → Result s₂ it ε α
        Equations
        Instances For
          source
          @[inline]
          def Regex.Syntax.Parser.Combinators.Result.transOr {s₁ s₂ : Bool} {it it' : String.Iterator} {ε α : Type} (h : Rel s₂ it' it) :
          Result s₁ it' ε α → Result (s₁ || s₂) it ε α
          Equations
          Instances For
            source
            @[inline]
            def Regex.Syntax.Parser.Combinators.Result.trans {s : Bool} {it it' : String.Iterator} {ε α : Type} (h : Rel s it it') :
            Result s it ε α → Result s it' ε α
            Equations
            Instances For
              source
              @[inline]
              def Regex.Syntax.Parser.Combinators.Result.cast {s₁ s₂ : Bool} {it : String.Iterator} {ε α : Type} (h : s₁ = s₂) (res : Result s₁ it ε α) :
              Result s₂ it ε α
              Equations
              Instances For
                source
                @[inline]
                def Regex.Syntax.Parser.Combinators.Result.weaken {s : Bool} {it : String.Iterator} {ε α : Type} (res : Result s it ε α) :
                Result false it ε α
                Equations
                Instances For
                  source
                  @[inline]
                  def Regex.Syntax.Parser.Combinators.Result.toExcept {s : Bool} {it : String.Iterator} {ε α : Type} (res : Result s it ε α) :
                  Except ε α
                  Equations
                  Instances For
                    source
                    @[inline]
                    def Regex.Syntax.Parser.Combinators.Result.opt {s : Bool} {it : String.Iterator} {ε α : Type} :
                    Result s it ε α → Result false it ε (Option α)
                    Equations
                    Instances For
                      source
                      @[inline]
                      def Regex.Syntax.Parser.Combinators.Result.complete {s : Bool} {it : String.Iterator} {ε α : Type} (expectedEof : ε) :
                      Result s it ε α → Result s it ε α
                      Equations
                      Instances For
                        source
                        @[inline]
                        def Regex.Syntax.Parser.Combinators.Result.commit {s : Bool} {it : String.Iterator} {ε α : Type} :
                        Result s it ε α → Result s it ε α
                        Equations
                        Instances For
                          source
                          @[inline]
                          def Regex.Syntax.Parser.Combinators.Result.guard {s : Bool} {it : String.Iterator} {ε α β : Type} (f : α → Except ε β) :
                          Result s it ε α → Result s it ε β
                          Equations
                          Instances For
                            source
                            @[inline]
                            def Regex.Syntax.Parser.Combinators.Result.map' {s : Bool} {it : String.Iterator} {ε α β : Type} (f : α → (it' : String.Iterator) → Rel s it' it → β) :
                            Result s it ε α → Result s it ε β
                            Equations
                            Instances For
                              source
                              @[inline]
                              def Regex.Syntax.Parser.Combinators.Result.map {s : Bool} {it : String.Iterator} {ε α β : Type} (f : α → β) :
                              Result s it ε α → Result s it ε β
                              Equations
                              Instances For
                                source
                                @[inline]
                                def Regex.Syntax.Parser.Combinators.Result.seq {s : Bool} {it : String.Iterator} {ε α β : Type} (mf : Result s it ε (α → β)) (mx : Unit → Result s it ε α) :
                                Result s it ε β
                                Equations
                                Instances For
                                  source
                                  @[inline]
                                  def Regex.Syntax.Parser.Combinators.Result.seqLeft {s : Bool} {it : String.Iterator} {ε α β : Type} (mx : Result s it ε α) (my : Unit → Result s it ε β) :
                                  Result s it ε α
                                  Equations
                                  Instances For
                                    source
                                    @[inline]
                                    def Regex.Syntax.Parser.Combinators.Result.seqRight {s : Bool} {it : String.Iterator} {ε α β : Type} (mx : Result s it ε α) (my : Unit → Result s it ε β) :
                                    Result s it ε β
                                    Equations
                                    Instances For
                                      source
                                      @[inline]
                                      def Regex.Syntax.Parser.Combinators.Result.hOrElse {s₁ s₂ : Bool} {it : String.Iterator} {ε α : Type} (mx : Result s₁ it ε α) (my : Unit → Result s₂ it ε α) :
                                      Result (s₁ && s₂) it ε α
                                      Equations
                                      Instances For
                                        source
                                        @[inline]
                                        def Regex.Syntax.Parser.Combinators.Result.orElse {s : Bool} {it : String.Iterator} {ε α : Type} :
                                        Result s it ε α → (Unit → Result s it ε α) → Result s it ε α
                                        Equations
                                        Instances For
                                          source
                                          @[inline]
                                          def Regex.Syntax.Parser.Combinators.Result.throw {s : Bool} {it : String.Iterator} {ε α : Type} (e : ε) :
                                          Result s it ε α
                                          Equations
                                          Instances For
                                            source
                                            @[inline]
                                            def Regex.Syntax.Parser.Combinators.Result.tryCatch {s : Bool} {it : String.Iterator} {ε α : Type} (mx : Result s it ε α) (handle : ε → Result s it ε α) :
                                            Result s it ε α
                                            Equations
                                            Instances For
                                              source
                                              @[inline]
                                              def Regex.Syntax.Parser.Combinators.Result.bind' {s₁ s₂ : Bool} {it : String.Iterator} {ε α β : Type} (mx : Result s₁ it ε α) (f : α → (it' : String.Iterator) → Rel s₁ it' it → Result s₂ it' ε β) :
                                              Result (s₁ || s₂) it ε β
                                              Equations
                                              Instances For
                                                source
                                                @[inline]
                                                def Regex.Syntax.Parser.Combinators.Result.bind {s : Bool} {it : String.Iterator} {ε α β : Type} (mx : Result s it ε α) (f : α → Result s it ε β) :
                                                Result s it ε β
                                                Equations
                                                Instances For
                                                  source
                                                  @[inline]
                                                  def Regex.Syntax.Parser.Combinators.Result.pure {it : String.Iterator} {ε α : Type} (a : α) :
                                                  LE it ε α
                                                  Equations
                                                  Instances For
                                                    source
                                                    @[inline]
                                                    instance Regex.Syntax.Parser.Combinators.Result.instFunctor {s : Bool} {it : String.Iterator} {ε : Type} :
                                                    Functor (Result s it ε)
                                                    Equations
                                                    source
                                                    @[inline]
                                                    instance Regex.Syntax.Parser.Combinators.Result.instSeq {s : Bool} {it : String.Iterator} {ε : Type} :
                                                    Seq (Result s it ε)
                                                    Equations
                                                    source
                                                    @[inline]
                                                    instance Regex.Syntax.Parser.Combinators.Result.instSeqLeft {s : Bool} {it : String.Iterator} {ε : Type} :
                                                    SeqLeft (Result s it ε)
                                                    Equations
                                                    source
                                                    @[inline]
                                                    instance Regex.Syntax.Parser.Combinators.Result.instSeqRight {s : Bool} {it : String.Iterator} {ε : Type} :
                                                    SeqRight (Result s it ε)
                                                    Equations
                                                    source
                                                    @[inline]
                                                    instance Regex.Syntax.Parser.Combinators.Result.instHOrElseAnd {s₁ s₂ : Bool} {it : String.Iterator} {ε α : Type} :
                                                    HOrElse (Result s₁ it ε α) (Result s₂ it ε α) (Result (s₁ && s₂) it ε α)
                                                    Equations
                                                    source
                                                    @[inline]
                                                    instance Regex.Syntax.Parser.Combinators.Result.instOrElse {s : Bool} {it : String.Iterator} {ε α : Type} :
                                                    OrElse (Result s it ε α)
                                                    Equations
                                                    source
                                                    @[inline]
                                                    instance Regex.Syntax.Parser.Combinators.Result.instMonadExceptOf {s : Bool} {it : String.Iterator} {ε : Type} :
                                                    MonadExceptOf ε (Result s it ε)
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    source
                                                    @[inline]
                                                    instance Regex.Syntax.Parser.Combinators.Result.instBind {s : Bool} {it : String.Iterator} {ε : Type} :
                                                    Bind (Result s it ε)
                                                    Equations
                                                    source
                                                    @[inline]
                                                    instance Regex.Syntax.Parser.Combinators.Result.instPureLE {it : String.Iterator} {ε : Type} :
                                                    Pure (LE it ε)
                                                    Equations
                                                    source
                                                    @[inline]
                                                    instance Regex.Syntax.Parser.Combinators.Result.instMonadLE {it : String.Iterator} {ε : Type} :
                                                    Monad (LE it ε)
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.