261 "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"} |
261 "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"} |
262 |
262 |
263 we can see the full name of the type is actually @{text "List.list"}, indicating |
263 we can see the full name of the type is actually @{text "List.list"}, indicating |
264 that it is defined in the theory @{text "List"}. However, one has to be |
264 that it is defined in the theory @{text "List"}. However, one has to be |
265 careful with names of types, because even if |
265 careful with names of types, because even if |
266 @{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the |
266 @{text "fun"} is defined in the theory @{text "HOL"}, it is |
267 theories @{text "HOL"} and @{text "Nat"}, respectively, they are |
|
268 still represented by their simple name. |
267 still represented by their simple name. |
269 |
268 |
270 @{ML_response [display,gray] |
269 @{ML_response [display,gray] |
271 "@{typ \"bool \<Rightarrow> nat\"}" |
270 "@{typ \"bool \<Rightarrow> nat\"}" |
272 "Type (\"fun\", [Type (\"HOL.bool\", []), Type (\"Nat.nat\", [])])"} |
271 "Type (\"fun\", [Type (\"HOL.bool\", []), Type (\"Nat.nat\", [])])"} |
382 in |
381 in |
383 lambda x_int trm |
382 lambda x_int trm |
384 end" |
383 end" |
385 "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"} |
384 "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"} |
386 |
385 |
387 then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted. |
386 then the variable @{text "Free (\"x\", \"nat\")"} is \emph{not} abstracted. |
388 This is a fundamental principle |
387 This is a fundamental principle |
389 of Church-style typing, where variables with the same name still differ, if they |
388 of Church-style typing, where variables with the same name still differ, if they |
390 have different type. |
389 have different type. |
391 |
390 |
392 There is also the function @{ML_ind subst_free in Term} with which terms can be |
391 There is also the function @{ML_ind subst_free in Term} with which terms can be |