exact Partrec'.of_part this.to_comp.partrec
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
this : Primrec fun v => if v.get i < v.get j then 1 else 0
⊢ Partrec' ↑fun v => (v.get i).isLtNat (v.get j)
no goals