Email Gateway (Aug 09 2022 at 02:31): Email Gateway (Aug 09 2022 at 02:31):From: Wenda Li <wl302@cam.ac.uk>
Dear locale experts,
I am curious if the behaviour of the following piece of code is as expected:
locale bar =
fixes G :: "'a list"
locale foo1 = bar
locale foo2 = bar R for R
consts f :: "'a list ⇒ ('a list) list"
sublocale foo1 < foo1 "f R" .
sublocale foo2 < foo2 "f R" .
(* The proof cannot be finished with the following exception:
"Roundup bound exceeded (sublocale relation probably not terminating)."
*)
Regards,
Wenda
Last updated: Jan 04 2025 at 20:18 UTC