equal
deleted
inserted
replaced
53 |
53 |
54 nominal_datatype sig_ass = |
54 nominal_datatype sig_ass = |
55 TC_ass "ident" "kind" |
55 TC_ass "ident" "kind" |
56 | C_ass "ident" "ty" |
56 | C_ass "ident" "ty" |
57 |
57 |
58 types Sig = "sig_ass list" |
58 type_synonym Sig = "sig_ass list" |
59 types Ctx = "(name \<times> ty) list" |
59 type_synonym Ctx = "(name \<times> ty) list" |
60 types Subst = "(name \<times> trm) list" |
60 type_synonym Subst = "(name \<times> trm) list" |
61 |
61 |
62 inductive |
62 inductive |
63 sig_valid :: "Sig \<Rightarrow> bool" ("\<turnstile> _ sig" [60] 60) |
63 sig_valid :: "Sig \<Rightarrow> bool" ("\<turnstile> _ sig" [60] 60) |
64 and ctx_valid :: "Sig \<Rightarrow> Ctx \<Rightarrow> bool" ("_ \<turnstile> _ ctx" [60,60] 60) |
64 and ctx_valid :: "Sig \<Rightarrow> Ctx \<Rightarrow> bool" ("_ \<turnstile> _ ctx" [60,60] 60) |
65 and trm_valid :: "Sig \<Rightarrow> Ctx \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_,_ \<turnstile> _ : _" [60,60,60,60] 60) |
65 and trm_valid :: "Sig \<Rightarrow> Ctx \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_,_ \<turnstile> _ : _" [60,60,60,60] 60) |