Computable Acc.rec and WellFounded.fix #

This file adds csimp theorems so that the compiler will be able to compile Acc.rec, WellFounded.fix and related operations.

Without this change, the following code will fail to compile as WellFounded.fix is noncomputable.

def log2p1 : Nat → Nat :=
  WellFounded.fix Nat.lt_wfRel.2 fun n IH =>
    let m := n / 2
    if h : m < n then
      IH m h + 1
    else
      0

source

@[implicit_reducible]

instance Acc.wfRel {α : Sort u_1} {r : α → α → Prop} :

WellFoundedRelation { val : α // Acc r val }

source

@[irreducible, specialize #[]]

def Acc.recC {α : Sort u_1} {r : α → α → Prop} {motive : (a : α) → Acc r a → Sort v} (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (hr : r y x) → motive y ⋯) → motive x ⋯) {a : α} (t : Acc r a) :

motive a t

A computable version of Acc.rec.

Instances For

source

@[csimp]

theorem Acc.rec_eq_recC :

@rec = @recC

source

@[reducible, inline]

abbrev Acc.ndrecC {α : Sort u_1} {r : α → α → Prop} {C : α → Sort v} (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) {a : α} (n : Acc r a) :

C a

A computable version of Acc.ndrec.

Instances For

source

@[csimp]

theorem Acc.ndrec_eq_ndrecC :

@ndrec = @ndrecC

source

@[reducible, inline]

abbrev Acc.ndrecOnC {α : Sort u_1} {r : α → α → Prop} {C : α → Sort v} {a : α} (n : Acc r a) (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) :

C a

A computable version of Acc.ndrecOn.

Instances For

source

@[csimp]

theorem Acc.ndrecOn_eq_ndrecOnC :

@ndrecOn = @ndrecOnC

source

@[inline]