Lean 3:
/-- Matches one out of a list of characters. -/
def one_of (cs : list char) : parser char :=
decorate_errors (do c ← cs, return c.to_string) $
sat (∈ cs)
Synport:
/-- Matches one out of a list of characters. -/
def oneOf (cs : List Charₓ) : Parser Charₓ :=
(decorateErrors do
let c ← cs
return c) <|
sat (· ∈ cs)Note that the .to_string disappears.
Lean 3:
Synport:
Note that the
.to_stringdisappears.