Theorems · Theorem · logic and foundations

Encodable.decode_list_succ

∀ {α : Type u_1} [inst : Encodable α] (v : ℕ),
  Encodable.decode v.succ =
    (fun x1 x2 => x1 :: x2) <$> Encodable.decode (Nat.unpair v).1 <*> Encodable.decode (Nat.unpair v).2

Defined in

Mathlib.Logic.Equiv.List

Cited by

0 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Encodable