cheri/sail_latexcc/sailccabsatom.tex


1
2
3
4
5
6
7

val abs_atom = {
  smt : "abs",
  ocaml: "abs_int",
  lem: "abs_int",
  c: "abs_int",
  coq: "abs_with_eq"
} : forall 'n. atom('n) -> {'o, 'o = #\hyperref[zabszyatom]{abs\_atom}#('n). atom('o)}