Stream: Beginner Questions

Topic: how to print the inductive hypothesis

view this post on Zulip ee (Apr 08 2024 at 13:14):

I;m trying to prove a lemma using list structures with an induction rule based on a function I defined, yet I'm not sure the inductive hypothesis is exactly what I need. How can I print it or just view it?
TIA

view this post on Zulip Maximilian Schäffeler (Apr 08 2024 at 15:37):

You can print the induction rule with thm f.induct, where f is the function you defined. print_statement f.induct may be a bit easier to read.

Last updated: Dec 21 2024 at 16:20 UTC