fixed indentation

parent 5c41a21e
......@@ -26,27 +26,27 @@ module M
S.length s1 = S.length s2 and
forall i:int. 0 <= i < S.length s1 -> S.get s1 i = S.get s2 i
let empty () =
{}
Str (S.create_length 0) 0 0
{ len result = 0 and inv result and eq (model result) (S.create_length 0) }
let length r =
{}
len r
{ result = len r }
let rec get r i =
{ inv r and 0 <= i < len r }
match r with
| Str s ofs len ->
S.get s (ofs + i)
| App l r _ ->
let n = length l in
if i < n then get l i else get r (i - n)
end
{ result = S.get (model r) i }
let empty () =
{}
Str (S.create_length 0) 0 0
{ len result = 0 and inv result and eq (model result) (S.create_length 0) }
let length r =
{}
len r
{ result = len r }
let rec get r i =
{ inv r and 0 <= i < len r }
match r with
| Str s ofs len ->
S.get s (ofs + i)
| App l r _ ->
let n = length l in
if i < n then get l i else get r (i - n)
end
{ result = S.get (model r) i }
end
(*
......
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