Re: [isabelle] type mappings

As with your other question, "*" simply denotes itself.

In any typedef, a non-empty set of an existing type is used to define the new type. Here, the relevant set is called "Prod". There is no automatic way to go from a type to its defining set, other than to find the actual typedef declaration.


On 16 Feb 2006, at 16:31, Sean McLaughlin wrote:


  Is there a way to determine, eg.
that the "*" type constructor corresponds to "Prod",
as in

typedef (Prod)
  ('a, 'b) "*"    (infixr 20)
    = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}"




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