stdlib: fixed string.OCaml.([])

was missing a precondition because the contract was written *after*
the function body, not before
parent 9111be29
......@@ -470,9 +470,10 @@ module OCaml
requires { 0 <= i < length s }
ensures { result = get s i }
let ([]) (s: string) (i: int63) : char = get s i
let ([]) (s: string) (i: int63) : char
requires { 0 <= i < length s }
ensures { result = get s i }
= get s i
val code (c: char) : int63
ensures { result = code c }
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment