liquid-fixpoint-0.8.0.2: tests/proof/sum.fq

fixpoint "--rewrite"

constant sum : (func(0, [int; int]))

define sum(n : int) : int = ((sum n) = if (n <= 0) then 0 else (n + sum (n-1)))

expand [1 : True]
expand [2 : True]

bind 0 n : {v : int | (3 <= v) }

constraint:
  env []
  lhs {v : int | true }
  rhs {v : int | (sum 5) = 15 }
  id 1 tag []