lean
lean copied to clipboard
feat(?): Better support for prod in well_founded
This is an attempt at following up on https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Well.20founded.20definition/near/205105727, which noted that the following didn't work without extra encouragement:
def test : list ℕ × list ℕ → list ℕ × list ℕ
| ([],m) := ([],m)
| (a::l,m) := test(l,m)
-- works with
-- using_well_founded {dec_tac := `[apply prod.lex.left, well_founded_tactics.default_dec_tac]}
I have no idea how to test this locally, unfortunately.
If you think this concept is flawed, feel free to close.
The current plan is actually to remove this file altogether, @bryangingechen has started here: #288