Skip to content

Commit

Permalink
Fix for adjusted Inductive syntax
Browse files Browse the repository at this point in the history
  • Loading branch information
myreen committed Nov 8, 2023
1 parent 2cb02d0 commit 7101a3f
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 16 deletions.
6 changes: 3 additions & 3 deletions candle/prover/candle_kernel_valsScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ∧
Expand Down
26 changes: 13 additions & 13 deletions candle/prover/candle_prover_invScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit 7101a3f

Please sign in to comment.