Skip to content
This repository has been archived by the owner on Aug 2, 2019. It is now read-only.

Commit

Permalink
Restrictions in wftype to do with Void.
Browse files Browse the repository at this point in the history 
Relates to microvm-meta/#43
  • Loading branch information
@mn200
mn200 committed Oct 9, 2015
1 parent 1439c77 commit eced7b4
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions uvmTypesScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -177,7 +177,7 @@ val (wftype_rules, wftype_ind, wftype_cases) = Hol_reln`

(∀vset retty argtys.
wftype smap vset retty ∧
(∀ty. ty ∈ set argtys ⇒ wftype smap vset ty)
(∀ty. ty ∈ set argtys ⇒ wftype smap vset ty ∧ ty ≠ Void)
⇒
wftype smap vset (FuncRef retty argtys)) ∧

Expand All @@ -188,7 +188,7 @@ val (wftype_rules, wftype_ind, wftype_cases) = Hol_reln`
wftype smap vset (UFuncPtr retty argtys)) ∧

(∀vset sz ty.
0 < sz ∧ wftype smap vset ty
0 < sz ∧ wftype smap vset ty ∧ ty ≠ Void
⇒
wftype smap vset (Array ty sz)) ∧

Expand All @@ -198,13 +198,13 @@ val (wftype_rules, wftype_ind, wftype_cases) = Hol_reln`
wftype smap vset (Vector ty sz)) ∧

(∀vset fixty varty.
wftype smap vset fixty ∧ wftype smap vset varty
wftype smap vset fixty ∧ wftype smap vset varty ∧ varty ≠ Void
⇒
wftype smap vset (Hybrid fixty varty)) ∧

(∀vset tag.
tag ∈ FDOM smap ∧ smap ' tag ≠ [] ∧
(∀ty. MEM ty (smap ' tag) ⇒ wftype smap (tag INSERT vset) ty)
(∀ty. MEM ty (smap ' tag) ⇒ wftype smap (tag INSERT vset) ty ∧ ty ≠ Void)
⇒
wftype smap vset (Struct tag))
`
Expand Down

1 comment on commit eced7b4

@mn200
Copy link
Contributor Author

@mn200 mn200 commented on eced7b4 Oct 9, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See microvm/microvm-meta#43

(I failed to get the cross-reference syntax correct in the commit message.)

Please sign in to comment.