You can make α an implicit parameter by wrapping it inside curly-braces instead of parenthesis.
def myLength {α : Type} (xs : List α) :=
match xs with
| [] => 0
| _ :: ys => 1 + myLength ys
4 Likes