4 lines
No EOL
136 B
Text
4 lines
No EOL
136 B
Text
logic min: int, int -> int
|
|
axiom min_ax: forall x,y:int. min(x,y) <= x
|
|
parameter r: int ref
|
|
let f (n:int) = {} r := min !r n { r <= r@ } |