cheri/sail_latexcc/sailccdiv.tex


1
2
3
4
5
6
7

val div = {
  smt: "div",
  ocaml: "quotient",
  lem: "integerDiv",
  c: "tdiv_int",
  coq: "div_with_eq"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = #\hyperref[zdiv]{div}#('n, 'm). atom('o)}