Lines Matching defs:range
43 fun range NONE NONE = "Z"
44 | range (SOME i) NONE = "{n IN Z | " ^ Int.toString i ^ " <= n}"
45 | range NONE (SOME j) = "{n IN Z | n <= " ^ Int.toString j ^ "}"
46 | range (SOME i) (SOME j) =
55 SOME (arg ^ " option needs an integer argument in the range "
56 ^ range omin omax ^ " (not " ^ x ^ ")")}
72 fun range NONE NONE = "R"
73 | range (SOME i) NONE = "{n IN R | " ^ Real.toString i ^ " <= n}"
74 | range NONE (SOME j) = "{n IN R | n <= " ^ Real.toString j ^ "}"
75 | range (SOME i) (SOME j) =
84 SOME (arg ^ " option needs an real argument in the range "
85 ^ range omin omax ^ " (not " ^ x ^ ")")}