ink

def Mt.Utils.Fin.cast {n : Nat} {m : Nat} (i : Fin n) (eq : n = m) : Fin m

Equations

• Mt.Utils.Fin.cast i eq = { val := i.val, isLt := (_ : i.val < m) }