I am trying to learn set construction in Isabelle but I am failing.
Consider you want a function that gives you all natural numbers that are smaller than a given number. I thought this should work:

fun set_of_nats ::"'nat ⇒'nat set" where
  "set_of_nats b = {a |(a::nat). a < b}"

But it doesnt. Error:

Type unification failed: Variable 'nat::type not of sort ord

Type error in application: incompatible operand type

Operator:  (<) a :: ??'a ⇒ bool
Operand:   b :: 'nat

The same error also occurs when I do not construct the set dynamically but rather give it a fixed condition, e.g replace b with any nat, like 5. Error remains the same.

what am I doing wrong here? And how can Isabelle handle potentially infinite sets in such a case (imagine the comparison is not less than but rather greather then)