@@ -32,15 +32,15 @@ mutual
3232 JSArray : JArray n ts -> JSON (JSONArray n ts)
3333 JSObject : JObject fs -> JSON (JSONObject fs)
3434
35−using (ts : Vect JSONType n)
36− index : (i : Fin n) -> JSON (JSONArray n ts) -> JSON (index i ts)
37− index fO (JSArray (x :: xs)) = x
38− index (fS i) (JSArray (x :: xs)) = index i (JSArray xs)
39−
40−using (ts1 : Vect JSONType m, ts2 : Vect JSONType n)
41− (++) : JSON (JSONArray m ts1) ->
42− JSON (JSONArray n ts2) ->
43− JSON (JSONArray (m + n) (ts1 ++ ts2))
44− (JSArray []) ++ ys = ys
45− (JSArray (x :: xs)) ++ ys with ((JSArray xs) ++ ys)
46− | JSArray as = JSArray (x :: as)
35+index : (i : Fin n) -> JSON (JSONArray n ts) -> JSON (index i ts)
36+index fO (JSArray (x :: xs)) = x
37+index (fS i) (JSArray (x :: xs)) = index i (JSArray xs)
38+
39+infixl 8 ++
40+
41+(++) : JSON (JSONArray m ts1) ->
42+ JSON (JSONArray n ts2) ->
43+ JSON (JSONArray (m + n) (ts1 ++ ts2))
44+(++) (JSArray []) ys = ys
45+(++) (JSArray (x :: xs)) ys with ((JSArray xs) ++ ys)
46+ | (JSArray as) = JSArray (x :: as)