You should use the library-defined rem
function. The rem
function takes two ints, so you can't call it for an instance of num
; instead you could do something like
module I4nDivisibleby2
sig num {
val: Int
}
fact {
all n:num | rem[n.val, 4] = 0
}
assert even {
all n : num | rem[n.val, 2] = 0
}
check even // => no counterexample found