Fix for adjusted Inductive syntax

CakeML · Nov 8, 2023 · 7101a3f · 7101a3f
1 parent 2cb02d0
commit 7101a3f
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 16 deletions.
diff --git a/candle/prover/candle_kernel_valsScript.sml b/candle/prover/candle_kernel_valsScript.sml
@@ -167,17 +167,17 @@ Inductive inferred:
 [~KernelFuns:]
   (∀ctxt f.
      f ∈ kernel_funs ⇒
-       inferred ctxt f) ∧
+       inferred ctxt f)
 [~TYPE:]
   (∀ctxt ty v.
      TYPE ctxt ty ∧
      TYPE_TYPE ty v ⇒
-       inferred ctxt v) ∧
+       inferred ctxt v)
 [~TERM:]
   (∀ctxt tm v.
      TERM ctxt tm ∧
      TERM_TYPE tm v ⇒
-       inferred ctxt v) ∧
+       inferred ctxt v)
 [~THM:]
   (∀ctxt th v.
      THM ctxt th ∧

diff --git a/candle/prover/candle_prover_invScript.sml b/candle/prover/candle_prover_invScript.sml
@@ -78,56 +78,56 @@ Inductive v_ok:
 [~Inferred:]
   (∀ctxt v.
      inferred ctxt v ⇒
-       kernel_vals ctxt v) ∧
+       kernel_vals ctxt v)
 [~PartialApp:]
   (∀ctxt f v g.
      kernel_vals ctxt f ∧
      v_ok ctxt v ∧
      do_partial_app f v = SOME g ⇒
-       kernel_vals ctxt g) ∧
+       kernel_vals ctxt g)
 [~KernelVals:]
   (∀ctxt v.
      kernel_vals ctxt v ⇒
-       v_ok ctxt v) ∧
+       v_ok ctxt v)
 [~Conv:]
   (∀ctxt opt vs.
      EVERY (v_ok ctxt) vs ∧
      (∀tag x. opt = SOME (TypeStamp tag x) ⇒ x ∉ kernel_types) ⇒
-       v_ok ctxt (Conv opt vs)) ∧
+       v_ok ctxt (Conv opt vs))
 [~Closure:]
   (∀ctxt env n x.
      env_ok ctxt env ∧
      safe_exp x ⇒
-       v_ok ctxt (Closure env n x)) ∧
+       v_ok ctxt (Closure env n x))
 [~Recclosure:]
   (∀ctxt env f n.
      env_ok ctxt env ∧
      EVERY safe_exp (MAP (SND o SND) f) ⇒
-       v_ok ctxt (Recclosure env f n)) ∧
+       v_ok ctxt (Recclosure env f n))
 [~Vectorv:]
   (∀ctxt vs.
      EVERY (v_ok ctxt) vs ⇒
-       v_ok ctxt (Vectorv vs)) ∧
+       v_ok ctxt (Vectorv vs))
 [~Lit:]
   (∀ctxt lit.
-     v_ok ctxt (Litv lit)) ∧
+     v_ok ctxt (Litv lit))
 [~FP_WordTree:]
   (∀ ctxt fp.
-     v_ok ctxt (FP_WordTree fp)) ∧
+     v_ok ctxt (FP_WordTree fp))
 [~FP_BoolTree:]
   (∀ ctxt fp.
-     v_ok ctxt (FP_BoolTree fp)) ∧
+     v_ok ctxt (FP_BoolTree fp))
 [~Real:]
   (∀ ctxt r.
-     v_ok ctxt (Real r)) ∧
+     v_ok ctxt (Real r))
 [~Loc:]
   (∀ctxt loc.
      loc ∉ kernel_locs ⇒
-       v_ok ctxt (Loc loc)) ∧
+       v_ok ctxt (Loc loc))
 [~Env:]
   (∀ctxt env ns.
      env_ok ctxt env ⇒
-       v_ok ctxt (Env env ns)) ∧
+       v_ok ctxt (Env env ns))
 [env_ok:]
   (∀ctxt env.
      (∀id len tag tn.