git.iko.soy/Idris-dev
on master help sign in
Merge pull request #886 from Melvar/append-fixity
d0343eeEdwin Brady
libs/javascript/JavaScript/JSON.idr−2
compare with master
unifiedsplit
@@ -36,8 +36,6 @@ index : (i : Fin n) -> JSON (JSONArray n ts) -> JSON (index i ts)
36index fZ (JSArray (x :: xs)) = x
36index fZ (JSArray (x :: xs)) = x
37index (fS i) (JSArray (x :: xs)) = index i (JSArray xs)
37index (fS i) (JSArray (x :: xs)) = index i (JSArray xs)
38
38
39−infixl 8 ++
40−
41(++) : JSON (JSONArray m ts1) ->
39(++) : JSON (JSONArray m ts1) ->
42 JSON (JSONArray n ts2) ->
40 JSON (JSONArray n ts2) ->
43 JSON (JSONArray (m + n) (ts1 ++ ts2))
41 JSON (JSONArray (m + n) (ts1 ++ ts2))
libs/prelude/Prelude/List.idr+1−2
@@ -12,8 +12,7 @@ import Prelude.Nat
12%access public
12%access public
13%default total
13%default total
14
14
15−infixr 7 ::
15+infixr 7 ::,++
16−infixl 8 ++
17
16
18%elim data List a
17%elim data List a
19 = Nil
18 = Nil