Zulip Chat Archive

Stream: mathlib4

Topic: Data.List.Perm

James Gallicchio (Jan 11 2023 at 03:59):

Setting up the branch & PR now :)

James Gallicchio (Jan 11 2023 at 04:40):

hm, this is weird -- Lean is having trouble showing these recursions are structural induction. Let me push so someone can take a look.

James Gallicchio (Jan 11 2023 at 04:42):

For List.Perm.symm I genuinely have no clue what is wrong. I'm gonna try to write it directly with rec (like it was in mathlib3) but I feel like the compiler should accept that definition

Johan Commelin (Jan 11 2023 at 04:44):

@James Gallicchio often it helps if you specify exactly which arguments you want to use in the induction step

Johan Commelin (Jan 11 2023 at 04:45):

  rw [my_lemma n]

instead of just

  rw [my_lemma]

James Gallicchio (Jan 11 2023 at 04:45):

Heh, I'm not even using tactic mode! I'll try writing out all arguments for my recursive calls

Last updated: Dec 20 2023 at 11:08 UTC