git.iko.soy/Idris-dev
on master help sign in
Explicit arguments in views
88c5385Edwin Brady
libs/base/Data/List/Views.idr+7−4
compare with master
unifiedsplit
@@ -27,7 +27,8 @@ public export
27data Split : List a -> Type where
27data Split : List a -> Type where
28 SplitNil : Split []
28 SplitNil : Split []
29 SplitOne : Split [x]
29 SplitOne : Split [x]
30+ SplitPair : {x, y : a} -> {xs, ys : List a} -> -- Explicit, don't erae
30− SplitPair : Split (x :: xs ++ y :: ys)
31+ Split (x :: xs ++ y :: ys)
31
32
32splitHelp : (head : a) ->
33splitHelp : (head : a) ->
33 (xs : List a) ->
34 (xs : List a) ->
@@ -53,8 +54,9 @@ split (x :: xs) = splitHelp x xs xs
53public export
54public export
54data SplitRec : List a -> Type where
55data SplitRec : List a -> Type where
55 SplitRecNil : SplitRec []
56 SplitRecNil : SplitRec []
56− SplitRecOne : SplitRec [x]
57+ SplitRecOne : {x : a} -> SplitRec [x]
58+ SplitRecPair : {xs, ys : List a} -> -- Explicit, don't erase
57− SplitRecPair : Lazy (SplitRec xs) -> Lazy (SplitRec ys) -> SplitRec (xs ++ ys)
59+ Lazy (SplitRec xs) -> Lazy (SplitRec ys) -> SplitRec (xs ++ ys)
58
60
59total
61total
60splitRecFix : (xs : List a) -> ((ys : List a) -> smaller ys xs -> SplitRec ys) ->
62splitRecFix : (xs : List a) -> ((ys : List a) -> smaller ys xs -> SplitRec ys) ->
@@ -76,7 +78,8 @@ splitRec xs = accInd splitRecFix xs (smallerAcc xs)
76public export
78public export
77data SnocList : List a -> Type where
79data SnocList : List a -> Type where
78 Empty : SnocList []
80 Empty : SnocList []
81+ Snoc : {x : a} -> {xs : List a} -> -- Explicit, so don't erase
79− Snoc : SnocList xs -> SnocList (xs ++ [x])
82+ SnocList xs -> SnocList (xs ++ [x])
80
83
81snocListHelp : SnocList xs -> (ys : List a) -> SnocList (xs ++ ys)
84snocListHelp : SnocList xs -> (ys : List a) -> SnocList (xs ++ ys)
82snocListHelp {xs} x [] = rewrite appendNilRightNeutral xs in x
85snocListHelp {xs} x [] = rewrite appendNilRightNeutral xs in x
libs/base/Data/Nat/Views.idr+4−4
@@ -2,14 +2,14 @@ module Data.Nat.Views
2
2
3public export
3public export
4data Half : Nat -> Type where
4data Half : Nat -> Type where
5− HalfOdd : Half (S (n + n))
5+ HalfOdd : {n : Nat} -> Half (S (n + n))
6− HalfEven : Half (n + n)
6+ HalfEven : {n : Nat} -> Half (n + n)
7
7
8public export
8public export
9data HalfRec : Nat -> Type where
9data HalfRec : Nat -> Type where
10 HalfRecZ : HalfRec Z
10 HalfRecZ : HalfRec Z
11− HalfRecEven : Lazy (HalfRec n) -> HalfRec (n + n)
11+ HalfRecEven : {n : Nat} -> Lazy (HalfRec n) -> HalfRec (n + n)
12− HalfRecOdd : Lazy (HalfRec n) -> HalfRec (S (n + n))
12+ HalfRecOdd : {n : Nat} -> Lazy (HalfRec n) -> HalfRec (S (n + n))
13
13
14export
14export
15half : (n : Nat) -> Half n
15half : (n : Nat) -> Half n
libs/prelude/Prelude/WellFounded.idr+2−2
@@ -22,8 +22,8 @@ data Accessible : (rel : a -> a -> Type) -> (x : a) -> Type where
22 ||| Accessibility
22 ||| Accessibility
23 |||
23 |||
24 ||| @ x the accessible element
24 ||| @ x the accessible element
25− ||| @ acc' a demonstration that all smaller elements are also accessible
25+ ||| @ rec a demonstration that all smaller elements are also accessible
26− Access : (acc' : (y : a) -> rel y x -> Accessible rel y) ->
26+ Access : (rec : (y : a) -> rel y x -> Accessible rel y) ->
27 Accessible rel x
27 Accessible rel x
28
28
29||| A relation `rel` on `a` is well-founded if all elements of `a` are
29||| A relation `rel` on `a` is well-founded if all elements of `a` are