cheri/sail_latexcc/sailccmod.tex


1
2
3
4
5
6
7

val mod = {
  smt: "mod",
  ocaml: "modulus",
  lem: "integerMod",
  c: "tmod_int",
  coq: "mod_with_eq"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = #\hyperref[zmod]{mod}#('n, 'm). atom('o)}