on 2ffd9e4 help sign in
1 line 58 B history raw
1take : (m : Fin 3) -> Vect 2 Nat -> Vect (finToNat m) Nat