@@ -3,7 +3,7 @@ module JSON
33import Data.SortedMap
44
55data JSONType : Type where
6− JSONArray : Vect JSONType n -> JSONType
6+ JSONArray : (n : Nat) -> Vect JSONType n -> JSONType
77 JSONString : JSONType
88 JSONNumber : JSONType
99 JSONBool : JSONType
@@ -13,9 +13,9 @@ data JSONType : Type where
1313mutual
1414 using (ts : Vect JSONType n, fs : SortedMap String JSONType)
1515 namespace JArray
16− data JArray : Vect JSONType n -> Type where
17− Nil : JArray []
18− (::) : JSON t -> JArray ts -> JArray (t :: ts)
16+ data JArray : (n : Nat) -> Vect JSONType n -> Type where
17+ Nil : JArray 0 []
18+ (::) : JSON t -> JArray n ts -> JArray (S n) (t :: ts)
1919
2020 namespace JObject
2121 data JObject : SortedMap String JSONType -> Type where
@@ -27,5 +27,10 @@ mutual
2727 JSNumber : Float -> JSON JSONNumber
2828 JSBool : Bool -> JSON JSONBool
2929 JSNull : JSON JSONNull
30− JSArray : JArray ts -> JSON (JSONArray ts)
30+ JSArray : JArray n ts -> JSON (JSONArray n ts)
3131 JSObject : JObject fs -> JSON (JSONObject fs)
32+
33+using (ts : Vect JSONType n)
34+ index : (i : Fin n) -> JSON (JSONArray n ts) -> JSON (index i ts)
35+ index fO (JSArray (x :: xs)) = x
36+ index (fS i) (JSArray (x :: xs)) = index i (JSArray xs)