Prove IsTypeRep AST_DEC_v in decProg

Author: myreen

compiler/bootstrap/translation/decProgScript.sml

@@ -34,4 +34,20 @@ val _ = register_type ``:locs``;
 val _ = register_type ``:exp``;
 val _ = register_type ``:dec``;
 
+Theorem IsTypeRep_AST_DEC_v:
+  IsTypeRep AST_DEC_v AST_DEC_TYPE
+Proof
+  irule_at Any (fetch_v_fun “:ast$dec” |> snd |> hd)
+  \\ irule_at Any (fetch_v_fun “:'a list” |> snd |> hd)
+  \\ rpt (irule_at Any (fetch_v_fun “:ast$exp” |> snd |> hd))
+  \\ rpt (irule_at Any (fetch_v_fun “:'a # 'b” |> snd |> hd))
+  \\ rpt (irule_at Any (fetch_v_fun “:ast$exp” |> snd |> hd))
+  \\ rpt (irule_at Any (fetch_v_fun “:ast$pat” |> snd |> hd))
+  \\ rpt (irule_at Any (fetch_v_fun “:ast$lit” |> snd |> hd))
+  \\ rpt (irule_at Any (fetch_v_fun “:word8” |> snd |> hd))
+  \\ rpt (irule_at Any (fetch_v_fun “:word64” |> snd |> hd))
+  \\ rpt (irule_at Any (fetch_v_fun “:string” |> snd |> hd))
+  \\ fs []
+QED
+
 val _ = export_theory();

compiler/repl/repl_init_envProgScript.sml

@@ -21,7 +21,7 @@ val env = get_ml_prog_state () |> get_env
 
 Triviality declare_env_thm:
   declare_env_rel ^s ^env
-    (^s with eval_state := SOME (EvalDecs (eval_state_var with env_id_counter := (0,1,0))))
+    (^s with eval_state := SOME (EvalDecs (eval_state_var with env_id_counter := (0,1,1))))
     (Env ^env (0,0))
 Proof
   fs [semanticPrimitivesTheory.declare_env_def,ml_progTheory.declare_env_rel_def]