Options for conversion/normalization

[favonia]

• --allows-empty-system: no ghcom etc
• --fhcom-kan=?: try different implementations of fcom and V types.
• --paranoid: normalize everything extremely eagarly
• --favonia: trolling mode

@mortberg What would be on your list to try out?

[jonsterling]

Another thing that I will soon be starting to try out is an experimental implementation of guarded cartesian cubical type theory. This is another natural choice for having a flag...

[jonsterling]

To support option switching, I just have to learn a bit better how this library works that I am using to generate the command-line frontend.

[jonsterling]

Another option/flag I want to support is "paranoid-mode" which runs the normalizer on all definitions as they are added to the proof state. We are using this right now to catch bugs, but it is very slow, and shouldn't be on by default.

[favonia]

After RedPRL/redtt#270.

[favonia]

Updates: We do support options, but the current code structure can be improved. In my opinion, we should replace the ad hoc option setting with reactive programming.

[favonia]

The general design issue I see is to use algebraic effects to communicate such preferences.