ATS factorial with proof

gistfile1.txt

/* From an example in the ATS distribution */
dataprop FACT (int, int) =
  | FACTzero (0, 1)
  | {n,r,r1:int | n > 0} FACTsucc (n, r) of (FACT (n-1, r1), MUL (n, r1, r))

fun fact {n:nat} .<n>. (n: int n): [r:int] (FACT (n, r) | int r) =
  if n > 0 then let
    val (pf1 | r1) = fact (n - 1)
    val (pf_mul | r) = n imul2 r1
  in
    (FACTsucc (pf1, pf_mul) | r)
  end else begin
    (FACTzero () | 1)
  end