[isabelle] typedef


i want to create a datatype

typedef less_three = {n€N. n<3}

Now, when we write

definition my_number  :: nat, where "my_number = 0.5"

then we get an error "0.5 is not a nat"

Now i want to get the same error with the type above less_three, meaning if i write

definition other_number :: three, where "other_number = 4"      (*)

then i want to get an error that "4 is not a less_three"  (cause its larger)

so basically an automatic type warning.

What bothers me is that the equation (*) above is just accepted by isabelle although its bad typed.

I have an idea what Rep and Abs do from the tutorial so i kinda understand, but still do you think u can give me an idea how to make the equation (*) produce an error?

Thank you!


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.