Re: [isabelle] overloaded defs



An overloaded constant simply refers to itself. There isn't a separate constant called "subset".

Larry


On 16 Feb 2006, at 14:37, Sean McLaughlin wrote:

  How do I find the actual constant an overloaded constant refers to?
Eg.

read "(A::bool set) <= (B :: bool set)";
val it =
Const ("op <=", "bool set => bool set => bool") $ Free ("A", "bool set") $
      Free ("B", "bool set") : Term.term

How do I find that "op <=" means "subset"?






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