Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Building a context_parser from a parser

view this post on Zulip Email Gateway (Aug 22 2022 at 20:18):

From: Joshua Chen <josh@joshchen.io>
Dear list,

What is the idiomatic way to build a 'a context_parser from a 'a parser? (I want the equivalent of Args.add but as a context parser.)

Cheers,
Josh

view this post on Zulip Email Gateway (Aug 22 2022 at 20:19):

From: Joshua Chen <josh@joshchen.io>
Alternatively, what is the idiom to chain parsers and context_parsers
together, say to parse arguments to methods?

Josh

view this post on Zulip Email Gateway (Aug 22 2022 at 20:19):

From: Joshua Chen <josh@joshchen.io>
I have found Scan.lift now, which I believe is the right way to convert
parsers to context_parsers. Just writing this here now for others'
future reference.

Last updated: Nov 21 2024 at 12:39 UTC