Re: [isabelle] Document preparation question

Am 17/01/2013 10:19, schrieb Joachim Breitner:
> 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"}

Not that I know. The original type is lost, so you have to write at least one
type, but to avoid writing two types you would need some ML (to check that the
type you give is the right one).


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