> Does Lean have a type for "list containing only prime powers"? You can wrap a base type with a proof which is called bundling inductive PrimePower where |

> Does Lean have a type for "list containing only prime powers"? You can wrap a base type with a proof which is called bundling inductive PrimePower where | mk (n : Nat) (prf : IsPrimePower n) So in this case the type checker will not allow construction unless the proof demonstrates they are prime powers The prf part gets erased at runtime so there's no overhead. You could also use a constraint/refinement type like you talked about and it's more flexible as it relates to using list operations like map filter reverse etc.