Write out steps

[Negabinary]

Adds a setting that forces the user to write out steps in the prover

[codecov]

Codecov Report

❌ Patch coverage is 0% with 239 lines in your changes missing coverage. Please review.
✅ Project coverage is 49.87%. Comparing base (e5bfb65) to head (321e69f).

Files with missing lines	Patch %	Lines
src/web/app/editors/stepper/MissingStep.re	0.00%	131 Missing ⚠️
src/web/app/editors/stepper/StepperBase.re	0.00%	42 Missing ⚠️
src/web/app/editors/stepper/WrittenStep.re	0.00%	35 Missing ⚠️
src/web/app/editors/stepper/RewriteChecker.re	0.00%	20 Missing ⚠️
src/web/app/editors/result/StepperEditor.re	0.00%	8 Missing ⚠️
src/web/Settings.re	0.00%	2 Missing ⚠️
src/language/CoreSettings.re	0.00%	1 Missing ⚠️

Additional details and impacted files

@@                   Coverage Diff                   @@
##           fix-infinite-lookup    #2111      +/-   ##
=======================================================
- Coverage                50.21%   49.87%   -0.35%     
=======================================================
  Files                      230      231       +1     
  Lines                    25436    25628     +192     
=======================================================
+ Hits                     12772    12781       +9     
- Misses                   12664    12847     +183     

Files with missing lines	Coverage Δ
src/web/view/NutMenu.re	0.00% <ø> (ø)
src/language/CoreSettings.re	0.00% <0.00%> (ø)
src/web/Settings.re	0.00% <0.00%> (ø)
src/web/app/editors/result/StepperEditor.re	0.00% <0.00%> (ø)
src/web/app/editors/stepper/RewriteChecker.re	0.00% <0.00%> (ø)
src/web/app/editors/stepper/WrittenStep.re	0.00% <0.00%> (ø)
src/web/app/editors/stepper/StepperBase.re	11.27% <0.00%> (-0.98%)	⬇️
src/web/app/editors/stepper/MissingStep.re	9.37% <0.00%> (-3.42%)	⬇️

... and 11 files with indirect coverage changes

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[cyrus-]

reflexivity isn't working in the inductive case

let id = fun x -> x in 
let map = 
fun (xs, f) -> 
case xs
| [] => []
| hd::tl => f(hd)::map(tl, f)
end
in
theorem test_thm = 
forall xs: [  ] -> 
map(xs, id) == xs
in map```

[cyrus-]

also the proof doesn't seem to work with built in map

[cyrus-]

• the up triangle in the pop up UI has a different height causing jitter in the UI when clicked on
• proofs about built in map (and presumably other built ins) not going through
• when check is valid, insert it immediately (also for algebrite)
• run checks on every edit rather than when clicked