lean4-cli icon indicating copy to clipboard operation
lean4-cli copied to clipboard

Avoiding manual conversion step & autocompletion

Open mhuisi opened this issue 4 years ago • 0 comments

When I have time to work on this again (in ~2 months), I'd like to adjust the API so that no extra conversion step is necessary at the end and work on autocompletion.

For the former, a macro approach could work well, where a type-safe output structure is generated either from a Parsed value or even directly at the start using the configuration macro. The library does not really track the real type right now, so the latter should be safer.

mhuisi avatar Feb 25 '21 22:02 mhuisi