Structured recursion

재귀의 일종. 모든 구조적 재귀는 유한한 절차 이내에 종료되는 게 보장된다. (ToDo: 정확한 정의 알아보기. 특히 Well-founded recursion과 차이점)

예시

주어진 자연수가 짝수인지 검사.

def even (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => not (even k)

이항 더하기 연산:

def plus (n : Nat) (k : Nat) : Nat :=
  match k with
  | Nat.zero => n
  | Nat.succ k' => Nat.succ (plus n k')