27 app :: "[term, term] \<Rightarrow> term" (infixl \<open>\<cdot>\<close> 20) and |
27 app :: "[term, term] \<Rightarrow> term" (infixl \<open>\<cdot>\<close> 20) and |
28 Has_type :: "[term, term] \<Rightarrow> typing" |
28 Has_type :: "[term, term] \<Rightarrow> typing" |
29 |
29 |
30 nonterminal context' and typing' |
30 nonterminal context' and typing' |
31 syntax |
31 syntax |
32 "_Trueprop" :: "[context', typing'] \<Rightarrow> prop" (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>_/ \<turnstile> _)\<close>) |
32 "_Trueprop" :: "[context', typing'] \<Rightarrow> prop" (\<open>(\<open>notation=judgment\<close>_/ \<turnstile> _)\<close>) |
33 "_Trueprop1" :: "typing' \<Rightarrow> prop" (\<open>(\<open>notation=\<open>prefix Trueprop\<close>\<close>_)\<close>) |
33 "_Trueprop1" :: "typing' \<Rightarrow> prop" (\<open>(\<open>notation=judgment\<close>_)\<close>) |
34 "" :: "id \<Rightarrow> context'" (\<open>_\<close>) |
34 "" :: "id \<Rightarrow> context'" (\<open>_\<close>) |
35 "" :: "var \<Rightarrow> context'" (\<open>_\<close>) |
35 "" :: "var \<Rightarrow> context'" (\<open>_\<close>) |
36 "_MT_context" :: "context'" (\<open>\<close>) |
36 "_MT_context" :: "context'" (\<open>\<close>) |
37 "_Context" :: "[typing', context'] \<Rightarrow> context'" (\<open>_ _\<close>) |
37 "_Context" :: "[typing', context'] \<Rightarrow> context'" (\<open>_ _\<close>) |
38 "_Has_type" :: "[term, term] \<Rightarrow> typing'" (\<open>(\<open>notation=\<open>infix Has_Type\<close>\<close>_:/ _)\<close> [0, 0] 5) |
38 "_Has_type" :: "[term, term] \<Rightarrow> typing'" (\<open>(\<open>notation=\<open>infix Has_Type\<close>\<close>_:/ _)\<close> [0, 0] 5) |