Re: [isabelle] Document preparation question

Hi Joachim,

> I’d like to use @{term_type foo} on expressions whose type contains a
> type synonym, but the result contains the unfolded type. Is there a
> better work-around than using
>         @{term "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒ Env"} at {text "::"} at {typ "heap ⇒ (exp ⇒ Value) ⇒ Env"}
> instead of just
>         @{term_type "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒ Env"}

I would suggest @{term_type [source] "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒

> @{abbrev ..} is nice. Can we have an @{type_abbrev ..} that
> pretty-prints the type equations?

Something to think about.

> Sometimes the lemmas would be clearer if free variables were explicitly
> all-quantified. Is there an easy way to achieve this (besides defining a
> variant of the lemma with an HOL-∀ in front)?

You could write a style in ML for the term antiquotation to add the
quantifiers to propositions. See the LaTeX sugar document for
fundamental hints, or just get back here.

> I also miss good ways to automatically print data type definitions. My
> work around is to show
>         lemma Terms:
>           "∃ x assn e'. (e = (Lam [x]. e') ∨ (e = Var x) ∨ (e = App e' x) ∨ (e = Let assn e'))"
>           by (metis Terms.exp_assn.exhaust(1))
> and pretty-print this lemma in the text, but a tool that formats an
> exhaust-lemma in the style of a grammar specification would be slick.

Maybe also something which can be implemented as term style, e.g.
expecting an exhaustivness lemma as produced by datatype and rearranging
it as desired.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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