Function phase_estimation_ty 

pub fn phase_estimation_ty() -> Expr

PhaseEstimation : ∀ (n : Nat), Prop Quantum phase estimation approximates the eigenvalue e^{2πiφ} of a unitary U to n bits of precision using n ancilla qubits and O(2^n) controlled-U applications.