Re: [isabelle] Opaque ascription for SML code generation



Hi  Jørgen,

> Hi,
> 
> Is there a way to make the SML code generator use opaque ascription "structure Foo :> FOO = struct ... end" rather than transparent ascription "structure Foo : FOO = struct ... end"?

the short answer is, no.

> OCaml does not have transparent ascription so perhaps the default for SML should be opaque ascription.

The Isabelle/ML tradition prevers abstypes over opaque ascriptions – as
far as I remember also pretty printing of values work better with
abstypes than opaque ascriptions.  When signatures have been added to
SML code generation, this pattern has been adopted.  Maybe it is time to
revisit that.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.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.