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.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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