Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] coinduct problem

view this post on Zulip Email Gateway (Aug 17 2022 at 14:47):

From: Temesghen Kahsai <lememta@gmail.com>
Hi all,

I am trying to prove a lemma by "coinduct".
I get the following error, at the point when I call "proof coinduct"

*** exception TERM raised: Expected 3 binop arguments
*** At command "proof".

What kind of error is that? any clue?
Thanks in advance for any advice.

-T

view this post on Zulip Email Gateway (Aug 17 2022 at 14:49):

From: Makarius <makarius@sketis.net>
Which version of Isabelle is this exactly (apparently some development
snapshot)? Can you produce an example that reproduces the error?

Makarius

Last updated: May 03 2024 at 08:18 UTC