tweak some type signatures

src/Quox/Context.idr

@@ -169,14 +169,14 @@ zipWith3Lazy : forall tm1, tm2, tm3, tm4.
                Telescope tm2 from to ->
                Telescope tm3 from to ->
                Telescope (\n => Lazy (tm4 n)) from to
-zipWith3Lazy f = zipWith3 (\x, y, z => delay $ f x y z)
+zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
 
 
 export
-lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
+lengthPrf : Telescope _ from to -> Subset Nat $ \len => len + from = to
 lengthPrf [<]        = Element 0 Refl
-lengthPrf (tel :< _) =
+lengthPrf (tel :< _) = let len = lengthPrf tel in
-  let len = lengthPrf tel in Element (S len.fst) (cong S len.snd)
+                       Element (S len.fst) (cong S len.snd)
 
 public export %inline
 length : Telescope {} -> Nat
@@ -196,40 +196,40 @@ parameters {auto _ : Monoid a}
   foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
 
   export %inline
-  fold : Telescope (\x => a) from to -> a
+  fold : Telescope' a from to -> a
   fold = foldMap id
 
   ||| like `fold` but calculate the elements only when actually appending
   export %inline
-  foldLazy : Telescope (\x => Lazy a) from to -> a
+  foldLazy : Telescope' (Lazy a) from to -> a
   foldLazy = foldMap force
 
 
 export %inline
-and : Telescope' (Lazy Bool) from to -> Bool
+and : Telescope' (Lazy Bool) _ _ -> Bool
 and = force . fold @{All}
 
 export %inline
-all : (forall n. f n -> Bool) -> Telescope f from to -> Bool
+all : (forall n. tm n -> Bool) -> Telescope tm _ _ -> Bool
 all p = and . map (delay . p)
 
 export %inline
-all2 : (forall n. f n -> g n -> Bool) ->
+all2 : (forall n. tm n -> tm2 n -> Bool) ->
-       Telescope f from to -> Telescope g from to -> Bool
+       Telescope tm from to -> Telescope tm2 from to -> Bool
 all2 p = and .: zipWithLazy p
 
 
 export %inline
-or : Telescope' (Lazy Bool) from to -> Bool
+or : Telescope' (Lazy Bool) _ _ -> Bool
 or = force . fold @{Any}
 
 export %inline
-any : (forall n. f n -> Bool) -> Telescope f from to -> Bool
+any : (forall n. tm n -> Bool) -> Telescope tm _ _ -> Bool
 any p = or . map (delay . p)
 
 export %inline
-any2 : (forall n. f n -> g n -> Bool) ->
+any2 : (forall n. tm1 n -> tm2 n -> Bool) ->
-       Telescope f from to -> Telescope g from to -> Bool
+       Telescope tm1 from to -> Telescope tm2 from to -> Bool
 any2 p = or .: zipWithLazy p