Re: [isabelle] quotient over record type



On Mi, 2013-02-20 at 09:21 -0800, Brian Huffman wrote:
> The problem here is that "my_record" is really just a type
> abbreviation for "unit my_record_ext".
> 
> (Question for the other Isabelle developers: How is an ordinary user
> supposed to discover what abbreviations like this stand for?)

Good question! The best way that I know is inspecting the output of
  ML_val {* @{typ my_record} |> dest_Type *}

Is there any simpler way?

Peter







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