Re: [isabelle] Fwd: Max of set in Isabelle



On Sa, 2013-01-19 at 22:05 -0800, Konstantin Weitz wrote:
> How can I find the maximum element in a set of numbers (nat) in Isabelle.
> The max function doesn't work, as it is only defined to take the maximum of
> two elements. I have an idea of how I could implement it using a reduce
> like function, but I don't know how to pick one random element from a set.


There's also a function Max:: 'a set => 'a

"Big_Operators.linorder_class.Max"
  :: "'a\<Colon>Orderings.linorder Set.set \<Rightarrow> 'a
\<Colon>Orderings.linorder"


Peter






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