Parsec utils for ReaderT and StateT

def Parsec.attemptM {ρ : Type} {σ : Type} {α : Type} (p : ReaderT ρ (StateT σ Lean.Parsec) α) : ReaderT ρ (StateT σ Lean.Parsec) α

extends Lean.Parsec.attempt

Equations

• One or more equations did not get rendered due to their size.

instance Parsec.instHOrElseParsecReaderTStateT_regex {α : Type} {ρ : Type} {σ : Type} : HOrElse (Lean.Parsec α) (ReaderT ρ (StateT σ Lean.Parsec) α) (ReaderT ρ (StateT σ Lean.Parsec) α)

Equations

• Parsec.instHOrElseParsecReaderTStateT_regex = { hOrElse := Parsec.orElseT }

def Parsec.tryCatchT {σ : Type} {α : Type} {β : Type} (p : StateT σ Lean.Parsec α) (csuccess : α → StateT σ Lean.Parsec β) (cerror : Unit → StateT σ Lean.Parsec β) : StateT σ Lean.Parsec β

extends Lean.Parsec.tryCatch

Equations

• One or more equations did not get rendered due to their size.

def Parsec.manyM {ρ : Type} {σ : Type} {α : Type} (p : ReaderT ρ (StateT σ Lean.Parsec) α) : ReaderT ρ (StateT σ Lean.Parsec) (Array α)

extends Lean.Parsec.many

Equations

• Parsec.manyM p = do let __do_lift ← read liftM (Parsec.manyCoreT (p __do_lift) #[])

def Parsec.failM {ρ : Type} {σ : Type} {α : Type} (msg : String) : ReaderT ρ (StateT σ Lean.Parsec) α

Equations

• Parsec.failM msg = liftM (Lean.Parsec.fail msg)

def Parsec.withPos {α : Type} (p : Lean.Parsec α) : Lean.Parsec (String.Pos × String.Pos × α)

Equations

• One or more equations did not get rendered due to their size.

def Parsec.withPosM {ρ : Type} {σ : Type} {α : Type} (p : ReaderT ρ (StateT σ Lean.Parsec) α) : ReaderT ρ (StateT σ Lean.Parsec) (String.Pos × String.Pos × α)

Equations

• One or more equations did not get rendered due to their size.

def Parsec.withPosSkip : Lean.Parsec String.Pos

Equations

• Parsec.withPosSkip = do let __discr ← Parsec.withPos Lean.Parsec.skip match __discr with | (fst, t, snd) => pure t

def Parsec.optSkipChar (c : Char) : Lean.Parsec Unit

Equations

• One or more equations did not get rendered due to their size.

def Parsec.optSkipString (s : String) : Lean.Parsec Unit

Equations

• Parsec.optSkipString s = do let __do_lift ← Lean.Parsec.peek? match __do_lift with | some val => Lean.Parsec.skipString s | none => pure ()

def Parsec.testChar (check : Char → Bool) : Lean.Parsec Bool

exec check on current char

Equations

• Parsec.testChar check = do let __do_lift ← Lean.Parsec.peek? match __do_lift with | some c => if check c = true then pure true else pure false | none => pure false

def Parsec.tryChar (check : Char → Bool) : Lean.Parsec (Option Char)

exec check on current char and consume char on success

Equations

• One or more equations did not get rendered due to their size.

def Parsec.trySkipChar (check : Char → Bool) : Lean.Parsec Bool

exec check on current char and skip char on success

Equations

• Parsec.trySkipChar check = do let __do_lift ← Parsec.tryChar check match __do_lift with | some val => pure true | x => pure false

def Parsec.tryCharThen {α : Type} (check : Char → Bool) (f : Char → α) (msg : optParam String "") : Lean.Parsec α

exec check on current char and then exec f on consumed char on success

Equations

• Parsec.tryCharThen check f msg = do let __do_lift ← Parsec.tryChar check match __do_lift with | some c => pure (f c) | x => Lean.Parsec.fail msg

def Parsec.tryCharMap {α : Type} (check : Char → Bool) (f : Char → α) : Lean.Parsec (Option α)

exec check on current char and map f on consumed char on success

Equations

• Parsec.tryCharMap check f = do let __do_lift ← Parsec.tryChar check match __do_lift with | some c => pure (some (f c)) | x => pure none

def Parsec.tryCharThenPWithPos {α : Type} (check : Char → Bool) (p : Lean.Parsec α) : Lean.Parsec (Option (String.Pos × String.Pos × α))

exec check on current char and then exec p on success

Equations

• One or more equations did not get rendered due to their size.

def Parsec.tryCharThenPWithPosM {ρ : Type} {σ : Type} {α : Type} (check : Char → Bool) (p : ReaderT ρ (StateT σ Lean.Parsec) α) : ReaderT ρ (StateT σ Lean.Parsec) (Option (String.Pos × String.Pos × α))

exec check on current char and then exec p on success

Equations

• One or more equations did not get rendered due to their size.

def Parsec.tryCharWithPos (check : Char → Bool) : Lean.Parsec (Option (String.Pos × String.Pos × Char))

Equations

• Parsec.tryCharWithPos check = Parsec.tryCharThenPWithPos check Lean.Parsec.anyChar

def Parsec.tryCharWithPosMap {α : Type} (check : Char → Bool) (f : Char → String.Pos → String.Pos → α) : Lean.Parsec (Option α)

Equations

• Parsec.tryCharWithPosMap check f = do let __do_lift ← Parsec.tryCharWithPos check match __do_lift with | some (p1, p2, c) => pure (some (f c p1 p2)) | x => pure none