Removed cheats about duplicat constructos in REPL
Close to proving nice characterisation of left-recursion.
get rid of the stop_list type

unnecessary since doing a fold of compile_dec1 anyway?
rename the eval compile_decs to fold_compile_top

because there's already a different compile_decs in compilerTheory
move bootstrapProofs into compiler/proofs, and move fold_compile_top into it

the theorem required for bootstrapping shouldn't have to depend on the
bootstrapping evaluation theory (it's slightly more general).
not sure if compile_repl_step still builds - will try asap
rework compile_repl_step to use compile_decs from the compiler

no separate fold_compile_top function. this means the bootstrap will
happen as if inside a module, but that shouldn't matter. although the
correctness theorem might require something to set up and destroy the
exception handler on the outside...
a theorem about env_rs holding for the really-empty initial states
bootstrap theorem statement that typechecks, but is probably false

as indicated in the comment.

the issue seems to be figuring out exactly how/what to say to connect
the semantic environment to the bytecode state... since this bytecode
state is kind of in the middle of any semantic breakpoint (just about to
make a function call)
notes on call_decl_thm statement

with magnus
removing stop_CONS may have been a mistake, trying stop_APPEND now

there's presumably no need to actually evaluate the APPEND of the new
code onto the old code between declarations.
minor corrections to lexer
lexer fixed and verified
Code to run the pretry printer and the parse the result.

Alas this immediately shows up an error in the pretty printer:

In CakeML, only constructors can start with capital letters, but the
translation of the HOL function "FST" has a non-constructor that starts
with "F".
eval_decs' to eval_decs

Brought the eval_dec' to eval_dec result to the decs level and prepare
for integration with the translator with DeclAssum2_thm in
ml_translatorScript.sml.
Start to work on evaluating the initial program into the initial environment
Prove completeness for common left-recursive parsing pattern.
Prove a better version of peg_linfix_complete and use it successfully.
Delete implausible (commented out) proof attempt on completeness.

The other approach is still looking plausible.
Modify the grammar to make completeness proof easier.

I've introduced a redundant non-terminal so that my linfix-lemma
applies to the TyVarList rule.
Extract my common tactics/theorems into a "parsing preamble" module.