equal
deleted
inserted
replaced
364 abbreviation |
364 abbreviation |
365 rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |-\<^sub>R _ : _" [50, 50, 50] 50) |
365 rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |-\<^sub>R _ : _" [50, 50, 50] 50) |
366 "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping" |
366 "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping" |
367 |
367 |
368 abbreviation (xsymbols) |
368 abbreviation (xsymbols) |
369 rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50) |
369 rtyping_rel1 :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50) |
370 "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T" |
370 "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T" |
371 |
371 |
372 inductive rtyping |
372 inductive rtyping |
373 intros |
373 intros |
374 Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T" |
374 Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T" |