Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Strange errors by coinductive command with boo...

Email Gateway (May 05 2024 at 09:03):

From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
Hi List,

there seems to be a problem when a coinductive predicate has Boolean
parameters.

I ran into this when trying to characterize the set of sequences of bool
that do not end in True^\omega or False^\omega.

While there might be better ways than the below approach, I got some
puzzling errors out of coinductive that might be worth reporting. It
seems that a parameter of type bool gets some special treatment. Is this
documented/expected behavior?

Problems occur on 2023 and RC-3.

Last updated: Jan 04 2025 at 20:18 UTC