Lines Matching defs:is
37 ourselves (the last component of each tuple is the function's
58 'x = 42 div 0' is unsatisfiable. Similar for div/mod on integers. *)
110 fail if the second argument is 0 or not a numeral *)
129 (* bv-shl is an undocumented Yices feature (as of version 1.0.29) *)
298 (* cannot be defined as a function in Yices because it is polymorphic *)
308 (* cannot be defined as a function in Yices because it is polymorphic *)
316 (* cannot be defined as a function in Yices because it is polymorphic *)
343 "index into bit-vector is not a numeral")
355 "word_extract: upper index is not a numeral")
359 "word_extract: lower index is not a numeral")
535 "not a data type constructor (range type is not a data type)"
544 is still missing. *)
604 "not a case constant (last argument is not a data type)"
616 is identical to the field selector name may already be
651 is identical to the field update function's name may already be
709 (* returns the eta-long form of a term, i.e., every variable/constant is
723 else (* 'rand' is a variable/constant *)