Agda does too! https://plfa.github.io/ for examples