@@ -20,7 +20,9 @@ mutual
2020 namespace JObject
2121 data JObject : SortedMap String JSONType -> Type where
2222 Nil : JObject empty
23− (::) : (f : (String, JSON t)) -> JObject fs -> JObject (insert (fst f) t fs)
23+ (::) : (f : (String, JSON t)) ->
24+ JObject fs ->
25+ JObject (insert (fst f) t fs)
2426
2527 data JSON : JSONType -> Type where
2628 JSString : String -> JSON JSONString
@@ -35,10 +37,10 @@ using (ts : Vect JSONType n)
3537 index fO (JSArray (x :: xs)) = x
3638 index (fS i) (JSArray (x :: xs)) = index i (JSArray xs)
3739
38−using(ts1 : Vect JSONType m, ts2 : Vect JSONType n)
40+using (ts1 : Vect JSONType m, ts2 : Vect JSONType n)
3941 (++) : JSON (JSONArray m ts1) ->
4042 JSON (JSONArray n ts2) ->
4143 JSON (JSONArray (m + n) (ts1 ++ ts2))
42− (JSArray []) ++ ys = ys
44+ (JSArray []) ++ ys = ys
4345 (JSArray (x :: xs)) ++ ys with ((JSArray xs) ++ ys)
4446 | JSArray as = JSArray (x :: as)