424 E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow> |
424 E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow> |
425 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts" |
425 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts" |
426 |
426 |
427 |
427 |
428 syntax (* for purely static typing *) |
428 syntax (* for purely static typing *) |
429 wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50) |
429 "_wt" :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50) |
430 wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50) |
430 "_wt_stmt" :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50) |
431 ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50) |
431 "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50) |
432 ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50) |
432 "_ty_var" :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50) |
433 ty_exprs_:: "env \<Rightarrow> [expr list, |
433 "_ty_exprs":: "env \<Rightarrow> [expr list, |
434 \<spacespace> ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50) |
434 \<spacespace> ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50) |
435 |
435 |
436 syntax (xsymbols) |
436 syntax (xsymbols) |
437 wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50) |
437 "_wt" :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50) |
438 wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50) |
438 "_wt_stmt" :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50) |
439 ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) |
439 "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) |
440 ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) |
440 "_ty_var" :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) |
441 ty_exprs_ :: "env \<Rightarrow> [expr list, |
441 "_ty_exprs" :: "env \<Rightarrow> [expr list, |
442 \<spacespace> ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50) |
442 \<spacespace> ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50) |
443 |
443 |
444 translations |
444 translations |
445 "E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T" |
445 "E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T" |
446 "E\<turnstile>s\<Colon>\<surd>" == "E\<turnstile>In1r s\<Colon>Inl (PrimT Void)" |
446 "E\<turnstile>s\<Colon>\<surd>" == "E\<turnstile>In1r s\<Colon>Inl (PrimT Void)" |