85 This is one common source for puzzlement in Isabelle, which has |
85 This is one common source for puzzlement in Isabelle, which has |
86 tacitly eta-contracted the output. You obtain a similar result |
86 tacitly eta-contracted the output. You obtain a similar result |
87 with beta-redexes |
87 with beta-redexes |
88 |
88 |
89 @{ML_response_fake [display, gray] |
89 @{ML_response_fake [display, gray] |
90 "@{term \"(\<lambda>x y. x) 1 2\"} |
90 "@{term \"(\<lambda>(x::int) (y::int). x)\"} $ @{term \"1::int\"} $ @{term \"2::int\"} |
91 |> pretty_term @{context} |
91 |> pretty_term @{context} |
92 |> pwriteln" |
92 |> pwriteln" |
93 "1"} |
93 "1"} |
94 |
94 |
95 There is a configuration value to switch off the tacit eta-contraction (see |
95 There is a dedicated configuration value for switching off the tacit |
96 \ref{sec:printing}), but none for beta-contraction. So in certain cases you |
96 eta-contraction, namely @{ML_ind eta_contract in Syntax} (see Section |
97 might have to inspect the internal representation of a term, instead of |
97 \ref{sec:printing}), but none for beta-contractions. However you can avoid |
98 pretty printing it. Because of the alluded puzzlement that might arise from |
98 the beta-contractions by switching off abbreviation using the configuration |
99 this feature of Isabelle, it is certainly an acrane fact that you should |
99 value @{ML_ind show_abbrevs in Syntax}. For example |
100 keep in mind about pretty-printing terms. |
100 |
|
101 |
|
102 @{ML_response_fake [display, gray] |
|
103 "@{term \"(\<lambda>(x::int) (y::int). x)\"} $ @{term \"1::int\"} $ @{term \"2::int\"} |
|
104 |> pretty_term (Config.put show_abbrevs false @{context}) |
|
105 |> pwriteln" |
|
106 "(\<lambda>x y. x) 1 2"} |
101 |
107 |
102 Isabelle makes a distinction between \emph{free} variables (term-constructor |
108 Isabelle makes a distinction between \emph{free} variables (term-constructor |
103 @{ML Free} and written on the user level in blue colour) and |
109 @{ML Free} and written on the user level in blue colour) and |
104 \emph{schematic} variables (term-constructor @{ML Var} and written with a |
110 \emph{schematic} variables (term-constructor @{ML Var} and written with a |
105 leading question mark). Consider the following two examples |
111 leading question mark). Consider the following two examples |