Jan van Brügge (Jan 02 2022 at 19:12): Jan van Brügge (Jan 02 2022 at 19:12):I have a proof goal in the form of: g A B (λx. f A B (h x)) C D = foo and a theorem like: f ?A ?B (h ?x) ?y = bar ?x ?y that I want to use as an unfold rule. But the rule does not do anything because I need to eta-expand the lambda in my proof goal. How would I do that? (alternatively, getting rid of the ?y in the theorem would work too)
Manuel Eberl (Jan 02 2022 at 19:54):The abs_def attribute performs contraction of theorems of the form ?f ?x = ?g ?x. So you can just do my_unfold_rule[abs_def].
Jan van Brügge (Jan 02 2022 at 19:58):Thanks, that's exactly what I needed.
Notification Bot (Jan 02 2022 at 19:58):Jan van Brügge has marked this topic as resolved.
Last updated: Apr 23 2024 at 20:15 UTC