Email Gateway (Aug 18 2022 at 14:58): Email Gateway (Aug 18 2022 at 14:58):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi again!
I tried to build my own antiquotation for doing what I indicated in my
last mail and came up with the following code:
ML {*
fun output_names [name] = [Pretty.str name]
| output_names [n1, n2] = map Pretty.str [n1, " and ", n2]
| output_names names =
let val (ns, n) = split_last (map Pretty.str names) in
Pretty.commas ns @ [Pretty.str ", and ", n]
end
fun output_thm_name {context = ctxt, ...} names =
let val _ =
map (PureThy.get_thm (ProofContext.theory_of ctxt)) names
in
ThyOutput.output [Pretty.block (output_names names)]
end
val _ = ThyOutput.antiquotation "lemmas"
(Scan.repeat1 (Scan.lift Args.name)) output_thm_name
*}
text {*
Some theorems are: @{lemmas conjI disjE impI}. Or @{lemmas FalseE}
*}
My remaining question would be: How do I indicate, that the word "and"
should be printed as standard text?
cheers
chris
Last updated: Apr 24 2024 at 04:17 UTC