equal
deleted
inserted
replaced
164 @{ML_response_fake [display, gray] |
164 @{ML_response_fake [display, gray] |
165 "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})" |
165 "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})" |
166 "(1::nat, x::'a)"} |
166 "(1::nat, x::'a)"} |
167 |
167 |
168 where @{text 1} and @{text x} are displayed with their inferred type. |
168 where @{text 1} and @{text x} are displayed with their inferred type. |
169 Even more type information can be printed by setting |
169 Other configuration values that influence |
170 the reference @{ML_ind show_all_types in Syntax} to @{ML true}. |
|
171 In this case we obtain |
|
172 *} |
|
173 |
|
174 text {* |
|
175 @{ML_response_fake [display, gray] |
|
176 "let |
|
177 val show_all_types_ctxt = Config.put show_all_types true @{context} |
|
178 in |
|
179 pwriteln (pretty_term show_all_types_ctxt @{term \"(1::nat, x)\"}) |
|
180 end" |
|
181 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"} |
|
182 |
|
183 where now even @{term Pair} is written with its type (@{term Pair} is the |
|
184 term-constructor for products). Other configuration values that influence |
|
185 printing of terms include |
170 printing of terms include |
186 |
171 |
187 \begin{itemize} |
172 \begin{itemize} |
188 \item @{ML_ind show_brackets in Syntax} |
173 \item @{ML_ind show_brackets in Syntax} |
189 \item @{ML_ind show_sorts in Syntax} |
174 \item @{ML_ind show_sorts in Syntax} |