instance instFinEnumBitVec_sSA {w : ℕ} : FinEnum (BitVec w)

Equations

• instFinEnumBitVec_sSA = FinEnum.mk (2 ^ w) { toFun := fun (x : BitVec w) => x.toFin, invFun := fun (x : Fin (2 ^ w)) => { toFin := x }, left_inv := ⋯, right_inv := ⋯ }

instance instFinEnumBool_sSA : FinEnum Bool

Equations

• One or more equations did not get rendered due to their size.

instance finEnumUnit : FinEnum Unit

Equations

• finEnumUnit = FinEnum.mk 1 { toFun := fun (x : Unit) => 0, invFun := fun (x : Fin 1) => (), left_inv := finEnumUnit.proof_2, right_inv := finEnumUnit.proof_3 }

instance finEnumEmpty : FinEnum Empty

Equations

• finEnumEmpty = FinEnum.mk 0 { toFun := fun (x : Empty) => x.elim, invFun := fun (x : Fin 0) => x.elim0, left_inv := finEnumEmpty.proof_1, right_inv := finEnumEmpty.proof_2 }