[isabelle] Translating syntactic sugar



Hello,

I was wondering how to translate

"\forall s in S. t(s)" into a let expression where t :: nat * nat.

let ?p = "ALL s. s : S --> t s < 0" isn't right since it has the type bool
=> bool, right? I'd want ?p to have the type nat, right?

Thanks

Eg




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