Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Translating syntactic sugar

view this post on Zulip Email Gateway (Aug 18 2022 at 15:27):

From: Eg Gloor <egglue@gmail.com>
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

Last updated: Apr 19 2024 at 04:17 UTC