redtt Option support request

[ ] --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?

Jun 11 '18 12:06 favonia

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...

Jun 13 '18 12:06 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.

Jun 14 '18 06:06 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.

Jun 30 '18 15:06 jonsterling

Yet another option: the removal of inconsistent faces.

Jun 30 '18 17:06 favonia

After #270.

Oct 17 '18 08:10 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.

Nov 09 '18 06:11 favonia