search

uwplse / pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
MIT License
49 stars 9 forks source link

Syntax of commands feels awkward at times #82

Open Ptival opened 4 years ago

Ptival commented 4 years ago

Due to how organically the set of commands evolved, I feel like they are now slightly confusing. In:

Lift Module <fromType> <toType> in <fromModule> as <toModule>.

My brain expects the item that follows the keyword Module to be a module, but the module comes later...

Not sure what would work best, either of:

Lift <fromType> <toType> in Module <fromModule>as <toModule>.

or:

Lift Module <fromModule> as <toModule> lifting <fromType> to <toType>.

I don't love either, but something to consider...