Theory Int_Classify

theory Int_Classify
  imports Int_Exec
begin

section ‹Int instance of the generic check-discharge interface›

text ‹
  The check classifier is derived from Int's bundle: the Boolean recursion over
  \<^typ>‹exp›, the three-way classification, and the node-indexed bridge to
  \<^const>‹checks_proven› come from the comparison queries
  \<^const>‹int_less›/\<^const>‹int_eq› and the mode's evaluator, through the
  ‹int_tf› interpretation in \<^theory>‹Voblint_Analysis_Int.Int_Transfer›. Their
  soundness is ‹int_tf.check.classify_check_proved› and
  ‹int_tf.check.classify_check_refuted›.
›

end