Re: [isabelle] Printing instantiations



Hi Steve,

> I was wondering whether it's possible to print out the instantiations
> returned by Thm.first_order_match. Since it returns the type (ctyp * ctyp)
> list * (cterm * cterm) list, is there a way to convert this type to a
> string? I just want to test it to see what the instantiations look like.
> Should I actually bother?

for explorative purpose the ML function PolyML.makestring does a good
job.  Any serious printing of logical entities requires weaving the
desired appearance on the ML level, e.g.

  fn ts => commas (map (Syntax.string_of_term @{context}) ts)

for printing a list of terms as string.  In the system those string
conversions are used rarely, more likely output is assembled by means of
pretty printer entities (type Pretty.T).

  fn ts => Pretty.commas (map (Syntax.pretty_term @{context}) ts)

See the pretty.ML, library.ML, and syntax.ML modules for available
combinators.

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.