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

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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