Difficulty with a definition

Stream: new members

[Victor Correa]

Hello, I'm having a difficulty to define the function initsSl, that i saw in a book about functional programming.

structure SymList (a : Type) where
  lhs : List a
  rhs : List a
  ok : (lhs.isEmpty → rhs.isEmpty ∨ rhs.length = 1) ∧
       (rhs.isEmpty → lhs.isEmpty ∨ lhs.length = 1)
 deriving Repr

def initsl {a : Type} (sl : SymList a) : SymList a :=
  have ⟨lsl, rsl, _⟩ := sl
  match sl with
  | ⟨[], _, _⟩ => ⟨[], [], by simp⟩
  | ⟨_, [], _⟩ => ⟨[], [], by simp⟩
  | ⟨xs, ys, _⟩ => ⟨xs, ys.tail, by simp⟩

where the by simp don't resolve the goal. I tried some other tactics but they didn't work.

[Robert Maxton]

What's SymList?

[Robert Maxton]

(In general, if you hover over a multiline code block in Zulip and look in the top-right corner, you'll see an icon that links to the Lean playground, auto-populated with the content of the code block. Generally speaking, if you want help with code you'll want to make sure that you've included enough of your code that the Lean playground code works, or at least fails in the same way your code does.)

[Victor Correa]

Robert Maxton said:

(In general, if you hover over a multiline code block in Zulip and look in the top-right corner, you'll see an icon that links to the Lean playground, auto-populated with the content of the code block. Generally speaking, if you want help with code you'll want to make sure that you've included enough of your code that the Lean playground code works, or at least fails in the same way your code does.)

Oh, my bad. I have already changed the code.