Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] a question

Email Gateway (Aug 18 2022 at 16:23):

From: Tobias Nipkow <nipkow@in.tum.de>
In your second proof you have a free f that needs to be fixed. In
particular, you need to ensure that the type of f and of x and y fit
together. You should start with

fix f :: "'a" and x y :: "'a tree"

(I haven't tried it out...)

But writing all of this out by hand is painful. I recommend to use the

case (Node x f y)
...
show ?case

idiom to simplify your life.

Tobias

张欢欢 schrieb:

Last updated: Nov 21 2024 at 12:39 UTC