sailccsubatom.tex « sail_latexcc « cheri - sail - Formal specification language for ISAs

summary refs log tree commit diff

path: root/cheri/sail_latexcc/sailccsubatom.tex

blob: 437e2d4c750413b14bb59ec85e4a2c95cf2cb776 (plain)

1
2

val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm.
  (atom('n), atom('m)) -> atom('n - 'm)