有没有办法从战术模式或精益中的匹配表达式递归调用函数？

问题描述

尝试 #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 α,cases i with i0 ri,exact s_val_x,exact sget' (pred i) s_val_s,end

尝试 #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

精益在这两种情况下都会引发 unkNown identifier sget' 错误。我知道我可以从 ehh 模式守卫递归调用 sget'（不确定它们是如何正确调用的），但是有没有办法用战术和/或匹配表达式来做类似的事情？

解决方法

如果你使用方程编译器，你可以进行递归调用

def map (f : α → β) : list α → list β
| [] := []
| (a :: l) := f a :: map l

否则，您应该使用 induction 策略或显式递归函数之一（如 nat.rec）。