Reputation: 63
Attempt #1:
def sget' {α : Type} {n : ℕ} (i : ℕ) {h1 : n > 0} {h2 : i < n} (s: sstack α n) : α :=
begin
cases n with n0 nn,
begin
have f : false, from nat.lt_asymm h1 h1,
tauto,
end,
induction s,
cases s_val,
begin
have : stack.empty.size = 0, from @stack_size_0 α,
tauto,
end,
cases i with i0 ri,
exact s_val_x,
exact sget' (pred i) s_val_s,
end
Attempt #2:
def sget' {α : Type} {n : ℕ} (i : ℕ) {h1 : n > 0} {h2 : i < n} (s: sstack α n) : α :=
match i, s with
| 0, ⟨stack.push x s, _⟩ := x
| i, ⟨stack.push _ s, _⟩ := sget' (pred i) ⟨s, _⟩
| _, ⟨stack.empty, _⟩ := sorry -- just ignore this
Lean in both cases throws unknown identifier sget'
error. I know that I can call sget'
recursively from ehh pattern guards (not sure how they are properly called), but is there any way to do something like that with tactics and/or match expressions?
Upvotes: 1
Views: 174
Reputation: 146
You can do recursive calls if you use the equation compiler
def map (f : α → β) : list α → list β
| [] := []
| (a :: l) := f a :: map l
Otherwise you should use induction
tactic or one of the explicit recursor functions (like nat.rec
).
Upvotes: 1