Evaluation Distributions of Computations with BitVec

File for lemmas about evalDist and support involving BitVec.

@[simp]

theorem probOutput_ofFin_map {m : Type → Type u_1} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {n : ℕ} (mx : m (Fin (2 ^ n))) (x : BitVec n) : Pr[=x | BitVec.ofFin <$> mx] = Pr[=x.toFin | mx]

@[simp]

theorem probOutput_bitVec_toFin_map {m : Type → Type u_1} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {n : ℕ} (mx : m (BitVec n)) (x : Fin (2 ^ n)) : Pr[=x | BitVec.toFin <$> mx] = Pr[={ toFin := x } | mx]

instance instSampleableTypeBitVec (n : ℕ) : SampleableType (BitVec n)