Email Gateway (Nov 08 2024 at 12:18): Email Gateway (Nov 08 2024 at 12:18):From: Tobias Nipkow <nipkow@in.tum.de>
In the code snippet below I define an anti-quotation const_typ that
pretty-prints a constant and its type. It gives me this type for map (when used
in a document)
map :: ('a => 'aa) => 'a list => 'aa list
whereas "term map" (on the Isabelle toplevel) displays the usual type with 'b
instead of 'aa.
Presumably my anti-quotation needs to be improved?
Tobias
setup ‹
Document_Output.antiquotation_pretty_source \<^binding>‹const_typ›
(Scan.lift Parse.embedded_inner_syntax)
(fn ctxt => fn c =>
let val tc = Proof_Context.read_const {proper = false, strict = false}
ctxt c in
Pretty.block [Document_Output.pretty_term ctxt tc, Pretty.str " ::",
Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
end)
›
Last updated: Jan 04 2025 at 20:18 UTC