 ### Fix some documentation.

parent c656dc97
 ... ... @@ -48,7 +48,7 @@ module Puzzle8 use import Roberval use import array.Array (** All values in [balls(lo..hi-1)] are equal to [w], apart from balls[lb] (** All values in [balls(lo..hi-1)] are equal to [w], apart from [balls[lb]] which is smaller. *) predicate spec (balls: array int) (lo hi: int) (lb w: int) = 0 <= lo <= lb < hi <= length balls && ... ...
 ... ... @@ -239,8 +239,8 @@ function size_c (c:cont) : int = lemma size_c_pos: forall c: cont. size_c c >= 0 (** WhyML programs (declared with "let" instead of "function"), mutually recursive, resulting from de-functionalization *) (** WhyML programs (declared with [let] instead of [function]), mutually recursive, resulting from de-functionalization *) let rec continue_2 (c:cont) (v:int) : int variant { size_c c } ... ... @@ -349,7 +349,7 @@ function size_c (c:cont) (acc:nat) : nat = | A2 _ k -> S (size_c k acc) end (** WhyML programs (declared with "let" instead of "function"), (** WhyML programs (declared with [let] instead of [function]), mutually recursive, resulting from de-functionalization *) let rec continue_2 (c:cont) (v:int) : int ... ...
 ... ... @@ -46,7 +46,7 @@ module LinearProbing ensures { 0 <= result < n } = mod (hash k) n (** j lies between l and r, cyclically *) (** [j] lies between [l] and [r], cyclically *) predicate between (l j r: int) = l <= j < r || r < l <= j || j < r < l ... ...
 ... ... @@ -249,7 +249,7 @@ module Balance ensures { 2 <= result } function string_of_array (q: Array.array rope) (l u: int) : string (** q[u-1] + q[u-2] + ... + q[l] *) (** [q[u-1] + q[u-2] + ... + q[l]] *) axiom string_of_array_empty: forall q: Array.array rope, l: int. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!